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  841  rspcime  2937  abvor0dc  3545  exmidsssn  4334  euotd  4390  nn0eln0  4762  elabrex  5953  elabrexg  5954  riota5f  6055  nntri3  6760  modom  7098  fin0  7179  2omap  7308  omp1eomlem  7424  ctssdccl  7441  ismkvnex  7485  finacn  7550  acnccim  7628  nn1m1nn  9301  xrlttri3  10178  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xltadd1  10257  xsubge0  10262  xposdif  10263  xlesubadd  10264  xleaddadd  10268  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  fzaddel  10443  elfzomelpfzo  10627  xqltnle  10680  nnesq  11075  hashnncl  11212  zfz1isolemiso  11269  swrdspsleq  11417  mod2eq1n2dvds  12624  m1exp1  12646  dfgcd3  12765  dvdssq  12786  pcdvdsb  13077  pceq0  13079  issubg3  13972  lmss  15270  lmres  15272  eupth2lem3lem6fi  16626