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  2884  abvor0dc  3484  exmidsssn  4247  euotd  4300  nn0eln0  4669  elabrex  5828  elabrexg  5829  riota5f  5926  nntri3  6585  fin0  6984  omp1eomlem  7198  ctssdccl  7215  ismkvnex  7259  finacn  7318  acnccim  7386  nn1m1nn  9056  xrlttri3  9921  nltpnft  9938  ngtmnft  9941  xrrebnd  9943  xltadd1  10000  xsubge0  10005  xposdif  10006  xlesubadd  10007  xleaddadd  10011  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  fzaddel  10183  elfzomelpfzo  10362  xqltnle  10412  nnesq  10806  hashnncl  10942  zfz1isolemiso  10986  swrdspsleq  11123  mod2eq1n2dvds  12223  m1exp1  12245  dfgcd3  12364  dvdssq  12385  pcdvdsb  12676  pceq0  12678  issubg3  13561  lmss  14751  lmres  14753  2omap  15969