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  2770  abvor0dc  3356  exmidsssn  4095  euotd  4146  nn0eln0  4503  elabrex  5627  riota5f  5722  nntri3  6361  fin0  6747  omp1eomlem  6947  ctssdccl  6964  ismkvnex  6997  nn1m1nn  8706  xrlttri3  9551  nltpnft  9565  ngtmnft  9568  xrrebnd  9570  xltadd1  9627  xsubge0  9632  xposdif  9633  xlesubadd  9634  xleaddadd  9638  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  fzaddel  9807  elfzomelpfzo  9976  nnesq  10379  hashnncl  10510  zfz1isolemiso  10550  mod2eq1n2dvds  11503  m1exp1  11525  dfgcd3  11625  dvdssq  11646  lmss  12342  lmres  12344
  Copyright terms: Public domain W3C validator