Theorem anbi1d 469

Description: Deduction adding a right 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
anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 455	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi1  470  anbi12d  477  bi2anan9  614  pm5.71dc  974  dfifp4dc  996  dfifp5dc  997  xorbi1d  1430  drsb1  1852  ax11ev  1881  eleq1w  2299  eleq1  2301  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  vtocl2gaf  2890  alexeq  2952  ceqex  2953  elrabi  2979  sbc5  3075  rexss  3315  ineq1  3425  difin2  3493  r19.28m  3617  elif  3652  ifeqeqxdc  3687  rabsnifsb  3777  preq12bg  3898  opeq1  3904  eluni  3938  disjiun  4125  mpteq12f  4211  axsepg  4250  sepg  4251  zfausclOLD  4253  opthg  4378  copsexg  4384  euotd  4395  elopab  4400  pocl  4448  uniuni  4597  rabxfrd  4615  ontr2exmid  4672  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  preleq  4702  xpeq1  4788  elxpi  4790  vtoclr  4823  opbrop  4854  opelresg  5070  resopab2  5110  elxp4  5275  elxp5  5276  cnvpom  5330  fun11  5448  feq2  5517  f1eq2  5594  f1eq3  5595  foeq2  5612  brprcneu  5688  ssimaexg  5765  dmfco  5773  fndmdif  5814  respreima  5836  isoeq5  6011  isoini  6024  isopolem  6028  f1oiso  6032  f1oiso2  6033  riotaeqdv  6039  acexmidlemab  6079  acexmidlemcase  6080  oprabid  6117  mpoeq123  6147  mpoeq123dva  6149  eloprabga  6175  resoprab  6184  resoprab2  6185  ov  6208  ovi3  6226  ov6g  6227  ovg  6228  caoftrn  6335  opabex3d  6350  opabex3  6351  elxp7  6404  eloprabi  6432  cnvf1o  6461  xporderlem  6467  poxp  6468  rexsupp  6493  smoel2  6574  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnaordex  6801  qliftel  6889  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  th3q  6914  ixpsnf1o  7018  dom2lem  7058  mapsnend  7099  modom  7108  xpsnen  7119  xpassen  7128  pw2f1odclem  7134  xpf1o  7144  opabfi  7247  ctssdccl  7451  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  ltsonq  7765  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  elinp  7841  prnmaxl  7855  prnminu  7856  prarloclemlo  7861  prarloc  7870  genpdflem  7874  genpassl  7891  genpassu  7892  ltexprlemm  7967  recexprlemell  7989  recexprlemelu  7990  cauappcvgprlemdisj  8018  caucvgprlemnkj  8033  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  mulgt0sr  8145  ltresr  8206  axpre-lttrn  8251  axpre-mulgt0  8254  recexgt0  8910  apreap  8917  apreim  8933  aprcl  8976  aptap  8980  prime  9749  rexuz  9989  ltxr  10187  ixxval  10308  fzval  10423  hashfibclem  11296  hashf1lem2  11300  eqwrd  11359  pfxeq  11482  wrd2ind  11509  sqrtrval  11780  abslt  11869  absle  11870  lenegsq  11876  abs2difabs  11889  2clim  12083  climcn2  12091  addcn2  12092  mulcn2  12094  climrecvg1n  12130  sumeq1  12137  fsum2dlemstep  12217  modfsummod  12241  prodeq1f  12335  fprod2dlemstep  12405  nndivdvds  12579  divalg2  12709  gcdval  12752  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  gcdass  12808  lcmval  12857  lcmass  12879  rpexp  12948  pythagtriplem2  13065  pythagtrip  13082  gzsumfzval  13760  issgrpv  13768  issgrpn0  13769  ismhm  13817  mhmpropd  13822  issubm  13828  issubg  14025  issubg3  14044  ringpropd  14392  crngpropd  14393  opprunitd  14466  issubrg  14578  resrhm2b  14606  islmod  14676  lmodlema  14677  lmodprop2d  14734  islssm  14743  islssmg  14744  lsslss  14767  znleval  15037  psrbag  15102  istopg  15149  basis2  15198  tg2  15210  iscld  15253  neival  15293  isnei  15294  isneip  15296  iscn  15347  cnpval  15348  iscnp  15349  txbas  15408  txdis1cn  15428  ispsmet  15473  ismet  15494  isxmet  15495  ismet2  15504  blres  15584  elmopn  15596  mopni  15632  neibl  15641  metrest  15656  elcncf  15723  mulc1cncf  15739  mulcncf  15758  limccnp2lem  15826  sincosq2sgn  15978  sincosq4sgn  15980  pellexlem3  16150  2lgslem1a  16305  edgssv2en  16538  uhgr2edg  16545  vtxdfifiun  16636  trlsfvalg  16722  istrl  16724  clwwlknp  16756  iseupth  16786  eupth2lem2dc  16798  bdsep2  17010  bdsepg  17014  bj-d0clsepcl  17049  sscoll2  17112  wexmiddifxy  17144