Theorem 2thd 174

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 172	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biort  819  rspcime  2837  abvor0dc  3432  exmidsssn  4181  euotd  4232  nn0eln0  4597  elabrex  5726  riota5f  5822  nntri3  6465  fin0  6851  omp1eomlem  7059  ctssdccl  7076  ismkvnex  7119  nn1m1nn  8875  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xltadd1  9812  xsubge0  9817  xposdif  9818  xlesubadd  9819  xleaddadd  9823  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  fzaddel  9994  elfzomelpfzo  10166  nnesq  10574  hashnncl  10709  zfz1isolemiso  10752  mod2eq1n2dvds  11816  m1exp1  11838  dfgcd3  11943  dvdssq  11964  pcdvdsb  12251  pceq0  12253  lmss  12886  lmres  12888