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  824  rspcime  2841  abvor0dc  3438  exmidsssn  4188  euotd  4239  nn0eln0  4604  elabrex  5737  riota5f  5833  nntri3  6476  fin0  6863  omp1eomlem  7071  ctssdccl  7088  ismkvnex  7131  nn1m1nn  8896  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xltadd1  9833  xsubge0  9838  xposdif  9839  xlesubadd  9840  xleaddadd  9844  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzaddel  10015  elfzomelpfzo  10187  nnesq  10595  hashnncl  10730  zfz1isolemiso  10774  mod2eq1n2dvds  11838  m1exp1  11860  dfgcd3  11965  dvdssq  11986  pcdvdsb  12273  pceq0  12275  lmss  13040  lmres  13042