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

Theorem 2thd 173
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 171 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 61 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  abvor0dc  3304  euotd  4072  nn0eln0  4423  elabrex  5519  riota5f  5614  nntri3  6240  fin0  6581  nn1m1nn  8412  xrlttri3  9236  nltpnft  9248  ngtmnft  9249  xrrebnd  9250  iccshftr  9380  iccshftl  9382  iccdil  9384  icccntr  9386  fzaddel  9441  elfzomelpfzo  9607  nnesq  10038  hashnncl  10169  zfz1isolemiso  10209  mod2eq1n2dvds  10961  m1exp1  10983  dfgcd3  11081  dvdssq  11102
  Copyright terms: Public domain W3C validator