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  4341  euotd  4397  nn0eln0  4769  elabrex  5966  elabrexg  5967  riota5f  6068  nntri3  6775  modom  7114  fin0  7195  2omap  7324  omp1eomlem  7440  ctssdccl  7457  ismkvnex  7501  finacn  7566  acnccim  7644  nn1m1nn  9331  xrlttri3  10215  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xltadd1  10294  xsubge0  10299  xposdif  10300  xlesubadd  10301  xleaddadd  10305  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzaddel  10481  elfzomelpfzo  10665  xqltnle  10718  flaplt  10738  nnesq  11117  nn0sqdc  11167  hashnncl  11255  zfz1isolemiso  11312  swrdspsleq  11460  mod2eq1n2dvds  12670  m1exp1  12692  dfgcd3  12811  dvdssq  12832  pcdvdsb  13127  pceq0  13129  issubg3  14053  lmss  15489  lmres  15491  eupth2lem3lem6fi  16934