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  2872  abvor0dc  3471  exmidsssn  4232  euotd  4284  nn0eln0  4653  elabrex  5801  elabrexg  5802  riota5f  5899  nntri3  6552  fin0  6943  omp1eomlem  7155  ctssdccl  7172  ismkvnex  7216  nn1m1nn  9002  xrlttri3  9866  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xltadd1  9945  xsubge0  9950  xposdif  9951  xlesubadd  9952  xleaddadd  9956  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzaddel  10128  elfzomelpfzo  10301  xqltnle  10339  nnesq  10733  hashnncl  10869  zfz1isolemiso  10913  mod2eq1n2dvds  12023  m1exp1  12045  dfgcd3  12150  dvdssq  12171  pcdvdsb  12461  pceq0  12463  issubg3  13265  lmss  14425  lmres  14427