Theorem 2thd 240

Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)

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 238	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 60	1 |- ( ph -> ( ps <-> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  had1  1447  sbc2or  3183  abvor0  3643  ralidm  3771  disjprg  4276  euotd  4580  posn  4894  frsn  4896  cnvpo  5363  elabrex  5947  riota5f  6065  smoord  6812  brwdom2  7776  finacn  8208  acacni  8297  dfac13  8299  fin1a2lem10  8566  gch2  8829  gchac  8835  recmulnq  9120  nn1m1nn  10329  nn0sub  10617  qextltlem  11159  xsubge0  11211  xlesubadd  11213  iccshftr  11405  iccshftl  11407  iccdil  11409  icccntr  11411  fzaddel  11479  elfzomelpfzo  11612  sqlecan  11955  nnesq  11971  hashdom  12125  swrdspsleq  12325  repswsymballbi  12401  znnenlem  13476  bitsmod  13614  dvdssq  13726  pcdvdsb  13917  vdwmc2  14022  acsfn  14579  subsubc  14745  funcres2b  14789  isipodrs  15313  issubg3  15678  opnnei  18565  lmss  18743  lmres  18745  cmpfi  18852  xkopt  19069  acufl  19331  lmhmclm  20499  equivcmet  20667  degltlem1  21427  mdegle0  21432  cxple2  22026  rlimcnp3  22245  dchrelbas3  22461  tgcolg  22866  eupath2lem3  23422  isoun  25820  fz0n  27235  onint1  28142  ftc1anclem6  28313  gicabl  29296  dfacbasgrp  29306  sdrgacs  29400  bj-nfcsym  31986  lcvexchlem1  32249  ltrnatb  33351  cdlemg27b  33910