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

Step	Hyp	Ref	Expression
1		2thd.1	. 2 |- ( ph -> ps )
2		2thd.2	. 2 |- ( ph -> ch )
3		pm5.1im 173	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps <-> ch ) )

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  829  rspcime  2846  abvor0dc  3444  exmidsssn  4197  euotd  4248  nn0eln0  4613  elabrex  5749  riota5f  5845  nntri3  6488  fin0  6875  omp1eomlem  7083  ctssdccl  7100  ismkvnex  7143  nn1m1nn  8910  xrlttri3  9768  nltpnft  9785  ngtmnft  9788  xrrebnd  9790  xltadd1  9847  xsubge0  9852  xposdif  9853  xlesubadd  9854  xleaddadd  9858  iccshftr  9965  iccshftl  9967  iccdil  9969  icccntr  9971  fzaddel  10029  elfzomelpfzo  10201  nnesq  10609  hashnncl  10743  zfz1isolemiso  10787  mod2eq1n2dvds  11851  m1exp1  11873  dfgcd3  11978  dvdssq  11999  pcdvdsb  12286  pceq0  12288  lmss  13317  lmres  13319