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  2850  abvor0dc  3448  exmidsssn  4204  euotd  4256  nn0eln0  4621  elabrex  5760  elabrexg  5761  riota5f  5857  nntri3  6500  fin0  6887  omp1eomlem  7095  ctssdccl  7112  ismkvnex  7155  nn1m1nn  8939  xrlttri3  9799  nltpnft  9816  ngtmnft  9819  xrrebnd  9821  xltadd1  9878  xsubge0  9883  xposdif  9884  xlesubadd  9885  xleaddadd  9889  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzaddel  10061  elfzomelpfzo  10233  nnesq  10642  hashnncl  10777  zfz1isolemiso  10821  mod2eq1n2dvds  11886  m1exp1  11908  dfgcd3  12013  dvdssq  12034  pcdvdsb  12321  pceq0  12323  issubg3  13057  lmss  13831  lmres  13833