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

Theorem 2thd 175
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 173 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 62 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biort  830  rspcime  2863  abvor0dc  3461  exmidsssn  4220  euotd  4272  nn0eln0  4637  elabrex  5779  elabrexg  5780  riota5f  5877  nntri3  6523  fin0  6914  omp1eomlem  7124  ctssdccl  7141  ismkvnex  7184  nn1m1nn  8968  xrlttri3  9829  nltpnft  9846  ngtmnft  9849  xrrebnd  9851  xltadd1  9908  xsubge0  9913  xposdif  9914  xlesubadd  9915  xleaddadd  9919  iccshftr  10026  iccshftl  10028  iccdil  10030  icccntr  10032  fzaddel  10091  elfzomelpfzo  10263  xqltnle  10300  nnesq  10674  hashnncl  10810  zfz1isolemiso  10854  mod2eq1n2dvds  11919  m1exp1  11941  dfgcd3  12046  dvdssq  12067  pcdvdsb  12355  pceq0  12357  issubg3  13148  lmss  14223  lmres  14225
  Copyright terms: Public domain W3C validator