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  830  rspcime  2875  abvor0dc  3474  exmidsssn  4235  euotd  4287  nn0eln0  4656  elabrex  5804  elabrexg  5805  riota5f  5902  nntri3  6555  fin0  6946  omp1eomlem  7160  ctssdccl  7177  ismkvnex  7221  nn1m1nn  9008  xrlttri3  9872  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xltadd1  9951  xsubge0  9956  xposdif  9957  xlesubadd  9958  xleaddadd  9962  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzaddel  10134  elfzomelpfzo  10307  xqltnle  10357  nnesq  10751  hashnncl  10887  zfz1isolemiso  10931  mod2eq1n2dvds  12044  m1exp1  12066  dfgcd3  12177  dvdssq  12198  pcdvdsb  12489  pceq0  12491  issubg3  13322  lmss  14482  lmres  14484