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 rule). (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  3286  euotd  4038  nn0eln0  4388  elabrex  5450  riota5f  5544  nntri3  6162  fin0  6442  nn1m1nn  8160  xrlttri3  8984  nltpnft  8996  ngtmnft  8997  xrrebnd  8998  iccshftr  9128  iccshftl  9130  iccdil  9132  icccntr  9134  fzaddel  9189  elfzomelpfzo  9353  nnesq  9725  hashnncl  9856  mod2eq1n2dvds  10470  m1exp1  10492  dfgcd3  10590  dvdssq  10611
  Copyright terms: Public domain W3C validator