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  2871  abvor0dc  3470  exmidsssn  4231  euotd  4283  nn0eln0  4652  elabrex  5800  elabrexg  5801  riota5f  5898  nntri3  6550  fin0  6941  omp1eomlem  7153  ctssdccl  7170  ismkvnex  7214  nn1m1nn  9000  xrlttri3  9863  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xltadd1  9942  xsubge0  9947  xposdif  9948  xlesubadd  9949  xleaddadd  9953  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzaddel  10125  elfzomelpfzo  10298  xqltnle  10336  nnesq  10730  hashnncl  10866  zfz1isolemiso  10910  mod2eq1n2dvds  12020  m1exp1  12042  dfgcd3  12147  dvdssq  12168  pcdvdsb  12458  pceq0  12460  issubg3  13262  lmss  14414  lmres  14416