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  831  rspcime  2884  abvor0dc  3484  exmidsssn  4246  euotd  4299  nn0eln0  4668  elabrex  5826  elabrexg  5827  riota5f  5924  nntri3  6583  fin0  6982  omp1eomlem  7196  ctssdccl  7213  ismkvnex  7257  finacn  7316  acnccim  7384  nn1m1nn  9054  xrlttri3  9919  nltpnft  9936  ngtmnft  9939  xrrebnd  9941  xltadd1  9998  xsubge0  10003  xposdif  10004  xlesubadd  10005  xleaddadd  10009  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  fzaddel  10181  elfzomelpfzo  10360  xqltnle  10410  nnesq  10804  hashnncl  10940  zfz1isolemiso  10984  swrdspsleq  11120  mod2eq1n2dvds  12190  m1exp1  12212  dfgcd3  12331  dvdssq  12352  pcdvdsb  12643  pceq0  12645  issubg3  13528  lmss  14718  lmres  14720  2omap  15932