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  837  rspcime  2918  abvor0dc  3520  exmidsssn  4298  euotd  4353  nn0eln0  4724  elabrex  5908  elabrexg  5909  riota5f  6008  nntri3  6708  modom  7037  fin0  7117  omp1eomlem  7353  ctssdccl  7370  ismkvnex  7414  finacn  7479  acnccim  7551  nn1m1nn  9220  xrlttri3  10093  nltpnft  10110  ngtmnft  10113  xrrebnd  10115  xltadd1  10172  xsubge0  10177  xposdif  10178  xlesubadd  10179  xleaddadd  10183  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  fzaddel  10356  elfzomelpfzo  10539  xqltnle  10590  nnesq  10984  hashnncl  11120  zfz1isolemiso  11166  swrdspsleq  11314  mod2eq1n2dvds  12520  m1exp1  12542  dfgcd3  12661  dvdssq  12682  pcdvdsb  12973  pceq0  12975  issubg3  13859  lmss  15057  lmres  15059  eupth2lem3lem6fi  16412  2omap  16715