Theorem 2thd 173

Description: Two truths are equivalent (deduction rule). (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 171	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 61	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  abvor0dc  3269  euotd  4009  nn0eln0  4359  elabrex  5418  riota5f  5512  nntri3  6098  fin0  6369  nn1m1nn  8057  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  xrrebnd  8886  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzaddel  9077  elfzomelpfzo  9240  nnesq  9592  mod2eq1n2dvds  10279  m1exp1  10301  dfgcd3  10399  dvdssq  10420