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  2928  abvor0dc  3532  exmidsssn  4315  euotd  4371  nn0eln0  4742  elabrex  5930  elabrexg  5931  riota5f  6030  nntri3  6730  modom  7061  fin0  7142  2omap  7269  omp1eomlem  7385  ctssdccl  7402  ismkvnex  7446  finacn  7511  acnccim  7586  nn1m1nn  9255  xrlttri3  10130  nltpnft  10147  ngtmnft  10150  xrrebnd  10152  xltadd1  10209  xsubge0  10214  xposdif  10215  xlesubadd  10216  xleaddadd  10220  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fzaddel  10393  elfzomelpfzo  10576  xqltnle  10627  nnesq  11021  hashnncl  11158  zfz1isolemiso  11211  swrdspsleq  11359  mod2eq1n2dvds  12565  m1exp1  12587  dfgcd3  12706  dvdssq  12727  pcdvdsb  13018  pceq0  13020  issubg3  13909  lmss  15111  lmres  15113  eupth2lem3lem6fi  16466