Theorem anbi1d 465

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 451	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi1  466  anbi12d  473  bi2anan9  610  pm5.71dc  970  dfifp4dc  992  dfifp5dc  993  xorbi1d  1426  drsb1  1848  ax11ev  1877  eleq1w  2293  eleq1  2295  rexeqf  2738  reueq1f  2739  rmoeq1f  2740  rabeqf  2803  vtocl2gaf  2882  alexeq  2943  ceqex  2944  elrabi  2970  sbc5  3066  rexss  3305  ineq1  3415  difin2  3483  r19.28m  3599  elif  3634  rabsnifsb  3757  preq12bg  3877  opeq1  3883  eluni  3917  disjiun  4104  mpteq12f  4190  axsep2  4229  zfauscl  4230  opthg  4354  copsexg  4360  euotd  4371  elopab  4376  pocl  4424  uniuni  4572  rabxfrd  4590  ontr2exmid  4647  regexmidlemm  4654  regexmidlem1  4655  reg2exmidlema  4656  preleq  4677  xpeq1  4763  elxpi  4765  vtoclr  4798  opbrop  4829  opelresg  5045  resopab2  5085  elxp4  5250  elxp5  5251  cnvpom  5305  fun11  5423  feq2  5492  f1eq2  5569  f1eq3  5570  foeq2  5587  brprcneu  5663  ssimaexg  5739  dmfco  5745  fndmdif  5783  respreima  5805  isoeq5  5978  isoini  5991  isopolem  5995  f1oiso  5999  f1oiso2  6000  riotaeqdv  6004  acexmidlemab  6044  acexmidlemcase  6045  oprabid  6082  mpoeq123  6112  mpoeq123dva  6114  eloprabga  6140  resoprab  6149  resoprab2  6150  ov  6173  ovi3  6191  ov6g  6192  ovg  6193  caoftrn  6299  opabex3d  6314  opabex3  6315  elxp7  6364  eloprabi  6392  cnvf1o  6421  xporderlem  6427  poxp  6428  rexsupp  6453  smoel2  6534  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  nnaordex  6761  qliftel  6849  brecop  6859  eroveu  6860  ecopovtrn  6866  ecopovtrng  6869  th3qlem2  6872  th3q  6874  ixpsnf1o  6971  dom2lem  7011  mapsnend  7052  modom  7061  xpsnen  7072  xpassen  7081  pw2f1odclem  7087  xpf1o  7097  opabfi  7200  ctssdccl  7402  exmidapne  7574  dfplpq2  7669  dfmpq2  7670  ltsonq  7713  enq0sym  7747  enq0ref  7748  enq0tr  7749  enq0breq  7751  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  mulnnnq0  7765  elinp  7789  prnmaxl  7803  prnminu  7804  prarloclemlo  7809  prarloc  7818  genpdflem  7822  genpassl  7839  genpassu  7840  ltexprlemm  7915  recexprlemell  7937  recexprlemelu  7938  cauappcvgprlemdisj  7966  caucvgprlemnkj  7981  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  lttrsr  8077  mulgt0sr  8093  ltresr  8154  axpre-lttrn  8199  axpre-mulgt0  8202  recexgt0  8854  apreap  8861  apreim  8877  aprcl  8920  aptap  8924  prime  9677  rexuz  9912  ltxr  10108  ixxval  10229  fzval  10344  hashfibclem  11206  eqwrd  11265  pfxeq  11388  wrd2ind  11415  sqrtrval  11685  abslt  11773  absle  11774  lenegsq  11780  abs2difabs  11793  2clim  11986  climcn2  11994  addcn2  11995  mulcn2  11997  climrecvg1n  12033  sumeq1  12040  fsum2dlemstep  12120  modfsummod  12144  prodeq1f  12238  fprod2dlemstep  12308  nndivdvds  12482  divalg2  12612  gcdval  12655  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemex  12697  gcdass  12711  lcmval  12760  lcmass  12782  rpexp  12850  pythagtriplem2  12964  pythagtrip  12981  gsumfzval  13604  issgrpv  13617  issgrpn0  13618  ismhm  13674  mhmpropd  13679  issubm  13685  issubg  13890  issubg3  13909  ringpropd  14182  crngpropd  14183  opprunitd  14255  issubrg  14366  resrhm2b  14394  islmod  14439  lmodlema  14440  lmodprop2d  14496  islssm  14505  islssmg  14506  lsslss  14529  znleval  14801  psrbag  14817  istopg  14864  basis2  14913  tg2  14925  iscld  14968  neival  15008  isnei  15009  isneip  15011  iscn  15062  cnpval  15063  iscnp  15064  txbas  15123  txdis1cn  15143  ispsmet  15188  ismet  15209  isxmet  15210  ismet2  15219  blres  15299  elmopn  15311  mopni  15347  neibl  15356  metrest  15371  elcncf  15438  mulc1cncf  15454  mulcncf  15473  limccnp2lem  15541  sincosq2sgn  15692  sincosq4sgn  15694  pellexlem3  15847  2lgslem1a  15961  edgssv2en  16194  uhgr2edg  16201  vtxdfifiun  16292  trlsfvalg  16378  istrl  16380  clwwlknp  16412  iseupth  16442  eupth2lem2dc  16454  bdsep2  16656  bdzfauscl  16660  bj-d0clsepcl  16695  sscoll2  16758