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  834  rspcime  2914  abvor0dc  3515  exmidsssn  4286  euotd  4341  nn0eln0  4712  elabrex  5881  elabrexg  5882  riota5f  5981  nntri3  6643  fin0  7047  omp1eomlem  7261  ctssdccl  7278  ismkvnex  7322  finacn  7386  acnccim  7458  nn1m1nn  9128  xrlttri3  9993  nltpnft  10010  ngtmnft  10013  xrrebnd  10015  xltadd1  10072  xsubge0  10077  xposdif  10078  xlesubadd  10079  xleaddadd  10083  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  fzaddel  10255  elfzomelpfzo  10437  xqltnle  10487  nnesq  10881  hashnncl  11017  zfz1isolemiso  11061  swrdspsleq  11199  mod2eq1n2dvds  12390  m1exp1  12412  dfgcd3  12531  dvdssq  12552  pcdvdsb  12843  pceq0  12845  issubg3  13729  lmss  14920  lmres  14922  2omap  16359