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  7452  exmidapne  7627  dfplpq2  7722  dfmpq2  7723  ltsonq  7766  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  elinp  7842  prnmaxl  7856  prnminu  7857  prarloclemlo  7862  prarloc  7871  genpdflem  7875  genpassl  7892  genpassu  7893  ltexprlemm  7968  recexprlemell  7990  recexprlemelu  7991  cauappcvgprlemdisj  8019  caucvgprlemnkj  8034  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  lttrsr  8130  mulgt0sr  8146  ltresr  8207  axpre-lttrn  8252  axpre-mulgt0  8255  recexgt0  8911  apreap  8918  apreim  8934  aprcl  8977  aptap  8981  prime  9750  rexuz  9990  ltxr  10188  ixxval  10309  fzval  10424  hashfibclem  11298  hashf1lem2  11302  eqwrd  11361  pfxeq  11484  wrd2ind  11511  sqrtrval  11782  abslt  11871  absle  11872  lenegsq  11878  abs2difabs  11891  2clim  12086  climcn2  12094  addcn2  12095  mulcn2  12097  climrecvg1n  12133  sumeq1  12140  fsum2dlemstep  12220  modfsummod  12244  prodeq1f  12338  fprod2dlemstep  12408  nndivdvds  12582  divalg2  12712  gcdval  12755  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  gcdass  12811  lcmval  12860  lcmass  12882  rpexp  12951  pythagtriplem2  13068  pythagtrip  13085  gzsumfzval  13764  issgrpv  13772  issgrpn0  13773  ismhm  13821  mhmpropd  13826  issubm  13832  issubg  14029  issubg3  14048  ringpropd  14427  crngpropd  14428  opprunitd  14501  issubrg  14613  resrhm2b  14641  islmod  14711  lmodlema  14712  lmodprop2d  14769  islssm  14778  islssmg  14779  lsslss  14802  znleval  15072  psrbag  15137  istopg  15191  basis2  15240  tg2  15252  iscld  15295  neival  15335  isnei  15336  isneip  15338  iscn  15389  cnpval  15390  iscnp  15391  txbas  15450  txdis1cn  15470  ispsmet  15515  ismet  15536  isxmet  15537  ismet2  15546  blres  15626  elmopn  15638  mopni  15674  neibl  15683  metrest  15698  elcncf  15765  mulc1cncf  15781  mulcncf  15800  limccnp2lem  15868  sincosq2sgn  16020  sincosq4sgn  16022  pellexlem3  16192  bpos  16281  2lgslem1a  16373  edgssv2en  16606  uhgr2edg  16613  vtxdfifiun  16704  trlsfvalg  16790  istrl  16792  clwwlknp  16824  iseupth  16854  eupth2lem2dc  16866  bdsep2  17078  bdsepg  17082  bj-d0clsepcl  17117  sscoll2  17180  wexmiddifxy  17212