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  831  rspcime  2891  abvor0dc  3492  exmidsssn  4262  euotd  4317  nn0eln0  4686  elabrex  5849  elabrexg  5850  riota5f  5947  nntri3  6606  fin0  7008  omp1eomlem  7222  ctssdccl  7239  ismkvnex  7283  finacn  7347  acnccim  7419  nn1m1nn  9089  xrlttri3  9954  nltpnft  9971  ngtmnft  9974  xrrebnd  9976  xltadd1  10033  xsubge0  10038  xposdif  10039  xlesubadd  10040  xleaddadd  10044  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  fzaddel  10216  elfzomelpfzo  10397  xqltnle  10447  nnesq  10841  hashnncl  10977  zfz1isolemiso  11021  swrdspsleq  11158  mod2eq1n2dvds  12305  m1exp1  12327  dfgcd3  12446  dvdssq  12467  pcdvdsb  12758  pceq0  12760  issubg3  13643  lmss  14833  lmres  14835  2omap  16132