Theorem imbi1d 229

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
imbi1d	|- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 156	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	imim1d 74	. 2 |- ( ph -> ( ( ps -> th ) -> ( ch -> th ) ) )
4	1	biimpd 142	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	imim1d 74	. 2 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
6	3, 5	impbid 127	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12d  232  imbi1  234  imim21b  250  pm5.33  573  imordc  829  drsb1  1720  ax11v2  1741  ax11v  1748  ax11ev  1749  equs5or  1751  raleqf  2545  alexeq  2721  mo2icl  2771  sbc19.21g  2882  csbiebg  2945  ralss  3060  ssuni  3623  intmin4  3664  ssexg  3917  pocl  4058  frforeq1  4098  frforeq2  4100  frind  4107  ontr2exmid  4268  elirr  4284  en2lp  4297  tfisi  4328  vtoclr  4406  sosng  4431  fun11  4986  funimass4  5245  dff13  5428  f1mpt  5431  isopolem  5481  oprabid  5557  caovcan  5685  caoftrn  5756  dfsmo2  5925  qliftfun  6211  ecoptocl  6216  ecopovtrn  6226  ecopovtrng  6229  dom2lem  6275  ssfiexmid  6361  domfiexmid  6363  findcard  6372  findcard2  6373  findcard2s  6374  supmoti  6406  eqsupti  6409  suplubti  6413  supisoex  6422  ltsonq  6588  prarloclem3  6687  lttrsr  6939  mulextsr1  6957  axpre-lttrn  7050  axpre-mulext  7054  axcaucvglemres  7065  prime  8446  raluz  8666  indstr  8681  supinfneg  8683  infsupneg  8684  fz1sbc  9113  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  caucvgre  9867  maxleast  10099  rexanre  10106  rexico  10107  minmax  10112  addcn2  10149  mulcn2  10151  cn1lem  10152  zsupcllemstep  10341  zsupcllemex  10342  bezoutlemmain  10387  dfgcd2  10403  exprmfct  10519  prmdvdsexpr  10529  sqrt2irr  10541  pw2dvdslemn  10543  bj-rspgt  10596  bdssexg  10695