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  830  rspcime  2863  abvor0dc  3461  exmidsssn  4220  euotd  4272  nn0eln0  4637  elabrex  5779  elabrexg  5780  riota5f  5877  nntri3  6523  fin0  6914  omp1eomlem  7124  ctssdccl  7141  ismkvnex  7184  nn1m1nn  8968  xrlttri3  9829  nltpnft  9846  ngtmnft  9849  xrrebnd  9851  xltadd1  9908  xsubge0  9913  xposdif  9914  xlesubadd  9915  xleaddadd  9919  iccshftr  10026  iccshftl  10028  iccdil  10030  icccntr  10032  fzaddel  10091  elfzomelpfzo  10263  xqltnle  10300  nnesq  10674  hashnncl  10810  zfz1isolemiso  10854  mod2eq1n2dvds  11919  m1exp1  11941  dfgcd3  12046  dvdssq  12067  pcdvdsb  12355  pceq0  12357  issubg3  13148  lmss  14223  lmres  14225