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

Theorem 2thd 174
Description: Two truths are equivalent (deduction form). (Contributed by NM, 3-Jun-2012.) (Revised by NM, 29-Jan-2013.)
Hypotheses
Ref Expression
2thd.1  |-  ( ph  ->  ps )
2thd.2  |-  ( ph  ->  ch )
Assertion
Ref Expression
2thd  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem 2thd
StepHypRef Expression
1 2thd.1 . 2  |-  ( ph  ->  ps )
2 2thd.2 . 2  |-  ( ph  ->  ch )
3 pm5.1im 172 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 62 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  rspcime  2768  abvor0dc  3354  exmidsssn  4093  euotd  4144  nn0eln0  4501  elabrex  5625  riota5f  5720  nntri3  6359  fin0  6745  omp1eomlem  6945  ctssdccl  6962  ismkvnex  6995  nn1m1nn  8698  xrlttri3  9534  nltpnft  9548  ngtmnft  9551  xrrebnd  9553  xltadd1  9610  xsubge0  9615  xposdif  9616  xlesubadd  9617  xleaddadd  9621  iccshftr  9728  iccshftl  9730  iccdil  9732  icccntr  9734  fzaddel  9790  elfzomelpfzo  9959  nnesq  10362  hashnncl  10493  zfz1isolemiso  10533  mod2eq1n2dvds  11483  m1exp1  11505  dfgcd3  11605  dvdssq  11626  lmss  12321  lmres  12323
  Copyright terms: Public domain W3C validator