ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2thd Structured version   GIF version

Theorem 2thd 164
Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.) (Revised by NM, 29-Jan-2013.)
Hypotheses
Ref Expression
2thd.1 (φψ)
2thd.2 (φχ)
Assertion
Ref Expression
2thd (φ → (ψχ))

Proof of Theorem 2thd
StepHypRef Expression
1 2thd.1 . 2 (φψ)
2 2thd.2 . 2 (φχ)
3 pm5.1im 162 . 2 (ψ → (χ → (ψχ)))
41, 2, 3sylc 56 1 (φ → (ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  abvor0dc  3236  euotd  3982  nn0eln0  4284  elabrex  5340  riota5f  5435  nntri3  6014  nn1m1nn  7673  xrlttri3  8448  nltpnft  8460  ngtmnft  8461  xrrebnd  8462  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  fzaddel  8652  elfzomelpfzo  8817  nnesq  8981
  Copyright terms: Public domain W3C validator