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:  rspcime  2800  abvor0dc  3391  exmidsssn  4133  euotd  4184  nn0eln0  4541  elabrex  5667  riota5f  5762  nntri3  6401  fin0  6787  omp1eomlem  6987  ctssdccl  7004  ismkvnex  7037  nn1m1nn  8762  xrlttri3  9613  nltpnft  9627  ngtmnft  9630  xrrebnd  9632  xltadd1  9689  xsubge0  9694  xposdif  9695  xlesubadd  9696  xleaddadd  9700  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  fzaddel  9870  elfzomelpfzo  10039  nnesq  10442  hashnncl  10574  zfz1isolemiso  10614  mod2eq1n2dvds  11612  m1exp1  11634  dfgcd3  11734  dvdssq  11755  lmss  12454  lmres  12456