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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biort  841  rspcime  2937  abvor0dc  3545  exmidsssn  4339  euotd  4395  nn0eln0  4767  elabrex  5963  elabrexg  5964  riota5f  6065  nntri3  6770  modom  7108  fin0  7189  2omap  7319  omp1eomlem  7435  ctssdccl  7452  ismkvnex  7496  finacn  7561  acnccim  7639  nn1m1nn  9325  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xltadd1  10289  xsubge0  10294  xposdif  10295  xlesubadd  10296  xleaddadd  10300  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzaddel  10476  elfzomelpfzo  10660  xqltnle  10713  flaplt  10733  nnesq  11112  nn0sqdc  11162  hashnncl  11250  zfz1isolemiso  11307  swrdspsleq  11455  mod2eq1n2dvds  12665  m1exp1  12687  dfgcd3  12806  dvdssq  12827  pcdvdsb  13122  pceq0  13124  issubg3  14048  lmss  15438  lmres  15440  eupth2lem3lem6fi  16878