Theorem anbi2d 440

Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
anbi2d	⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	a1d 22	. 2 ⊢ (φ → (θ → (ψ ↔ χ)))
3	2	pm5.32d 426	1 ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi2  443  anbi12d  445  bi2anan9  526  dn1dc  853  xorbi2d  1253  dfbi3dc  1269  xordidc  1271  eleq2  2079  ceqsex2  2567  ceqsex6v  2571  vtocl2gaf  2593  ceqsrex2v  2649  mob2  2694  eqreu  2706  nelrdva  2719  psssstr  3024  undif4  3257  r19.27m  3291  ifbi  3321  preq12bg  3514  opeq2  3520  ralunsn  3538  intab  3614  opabbid  3792  opthg  3945  pocl  4010  ordelord  4063  ordtriexmid  4190  onsucsssucexmid  4192  tfisi  4233  xpeq2  4283  rabxp  4303  vtoclr  4311  opeliunxp  4318  posng  4335  opbrop  4342  rexiunxp  4401  elrnmpt1  4508  dfres2  4581  brcodir  4635  poltletr  4648  xp11m  4682  elxp4  4731  elxp5  4732  dffun4f  4840  fununi  4889  fneq2  4910  fnun  4927  feq3  4954  foeq3  5025  funfveu  5109  funbrfv  5133  ssimaexg  5156  fvopab3g  5166  fvopab3ig  5167  fvelrn  5219  fmptco  5251  fsn2  5258  elunirn  5326  isoeq2  5363  isoeq3  5364  isocnv2  5373  isoini  5378  isopolem  5382  f1oiso  5386  f1oiso2  5387  oprabbid  5477  cbvoprab3  5499  mpt2mptx  5514  mpt2fun  5522  ov  5539  ovi3  5556  ov6g  5557  ovg  5558  caoftrn  5655  f1o2ndf1  5768  xporderlem  5770  brtpos2  5784  brtposg  5787  dftpos4  5796  recseq  5839  tfrlem3-2  5845  tfrlem3-2d  5846  tfrlemi1  5863  tfrexlem  5866  frecsuc  5903  nnaordex  6007  brecop  6103  eroveu  6104  erovlem  6105  ecopovtrn  6110  ecopovtrng  6113  th3qlem1  6115  th3qlem2  6116  th3q  6118  recex  6243  recmulnqg  6244  ltsonq  6251  enq0sym  6281  enq0ref  6282  enq0tr  6283  enq0breq  6285  addnq0mo  6296  mulnq0mo  6297  addnnnq0  6298  mulnnnq0  6299  elinp  6322  prdisj  6340  prarloclem3  6345  prarloc  6351  distrlem5prl  6419  distrlem5pru  6420  ltexprlemell  6429  ltexprlemelu  6430  recexprlemm  6452  addsrmo  6484  mulsrmo  6485  addsrpr  6486  mulsrpr  6487  lttrsr  6503  mulgt0sr  6516  ltresr  6544  axpre-lttrn  6572  axpre-mulgt0  6574