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  836  rspcime  2916  abvor0dc  3517  exmidsssn  4291  euotd  4346  nn0eln0  4717  elabrex  5900  elabrexg  5901  riota5f  6000  nntri3  6667  modom  6996  fin0  7076  omp1eomlem  7295  ctssdccl  7312  ismkvnex  7356  finacn  7421  acnccim  7493  nn1m1nn  9163  xrlttri3  10034  nltpnft  10051  ngtmnft  10054  xrrebnd  10056  xltadd1  10113  xsubge0  10118  xposdif  10119  xlesubadd  10120  xleaddadd  10124  iccshftr  10231  iccshftl  10233  iccdil  10235  icccntr  10237  fzaddel  10296  elfzomelpfzo  10479  xqltnle  10530  nnesq  10924  hashnncl  11060  zfz1isolemiso  11106  swrdspsleq  11254  mod2eq1n2dvds  12460  m1exp1  12482  dfgcd3  12601  dvdssq  12622  pcdvdsb  12913  pceq0  12915  issubg3  13799  lmss  14996  lmres  14998  eupth2lem3lem6fi  16348  2omap  16652