Theorem anbi12d 458

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
anbi12d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		anbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi1d 454	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 453	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.38  573  pm5.17dc  851  orbididc  902  3anbi123d  1255  xorbi2d  1323  xorbi1d  1324  drsb1  1734  mopick  2033  clelab  2219  cbvrexf  2599  cbvreu  2602  cbvrexdva2  2609  cbvrab  2631  gencbvex  2679  rspce  2731  eqvincf  2756  ceqsrexv  2761  elrabf  2783  rexab2  2795  reu2  2817  reu6  2818  rmo4  2822  reu8  2825  reuind  2834  sbcan  2895  sbcang  2896  sbcabel  2934  rmob  2945  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  difjust  3014  injust  3018  eldif  3022  ssconb  3148  elin  3198  opeq1  3644  opeq2  3645  2ralunsn  3664  elunii  3680  csbunig  3683  eluniab  3687  cbvopab  3931  cbvopab1  3933  cbvopab2  3934  cbvopab1s  3935  cbvopab2v  3937  cbvmptf  3954  cbvmpt  3955  trel  3965  nalset  3990  elssabg  4005  mss  4077  exss  4078  opelopab2a  4116  poeq1  4150  pocl  4154  soeq1  4166  weeq1  4207  weeq2  4208  ordeq  4223  zfun  4285  snnex  4298  reusv3  4310  ontr2exmid  4369  regexmid  4379  onintexmid  4416  reg3exmid  4423  peano5  4441  limom  4456  nnregexmid  4462  vtoclr  4515  opeliunxp  4522  poinxp  4536  opbrop  4546  csbxpg  4548  opeliunxp2  4607  relop  4617  brcogw  4636  elrnmpt1  4718  elsnres  4782  dfres2  4797  inimasn  4882  xpcanm  4904  xpcan2m  4905  elxp4  4952  elxp5  4953  cnvsom  5008  sbcfung  5073  funopg  5082  fununi  5116  funcnvuni  5117  fneq1  5136  2elresin  5159  feq1  5179  sbcfng  5193  sbcfg  5194  f1eq1  5246  foeq1  5264  f1oeq1  5279  f1oeq2  5280  f1oeq3  5281  ffoss  5320  brprcneu  5333  fv3  5363  tz6.12f  5368  ssimaex  5400  fvopab3g  5412  fvopab3ig  5413  fvopab6  5435  fmptco  5503  elunirn  5583  f1imaeq  5592  foeqcnvco  5607  fliftfun  5613  fliftval  5617  isoeq1  5618  isoeq4  5621  isoini  5635  isopolem  5639  f1oiso2  5644  riotabidv  5648  cbvriota  5656  acexmid  5689  ovanraleqv  5714  cbvoprab1  5758  cbvoprab2  5759  cbvoprab12  5760  cbvmpt2x  5764  ov  5802  ovig  5804  ovg  5821  caovimo  5876  caoftrn  5918  opabex3d  5930  opabex3  5931  elxp6  5978  unielxp  5982  dfoprab4  6000  dfoprab4f  6001  fmpt2x  6008  xporderlem  6034  poxp  6035  cnvoprab  6037  f1od2  6038  opeliunxp2f  6041  sprmpt2  6045  isprmpt2  6046  dftpos4  6066  tpostpos  6067  smoiso  6105  tfrlem3ag  6112  tfrlem3a  6113  tfr0dm  6125  tfrlemisucaccv  6128  tfrlemiex  6134  tfrlemi1  6135  tfrlemi14d  6136  tfrexlem  6137  tfr1onlem3ag  6140  tfr1onlemsucaccv  6144  tfr1onlemex  6150  tfr1onlemaccex  6151  tfr1onlemres  6152  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllemex  6163  tfrcllemaccex  6164  tfrcllemres  6165  tfrcldm  6166  frec0g  6200  frecabcl  6202  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecsuc  6210  nnacan  6311  nnmcan  6318  nnaordex  6326  ertr  6347  brecop  6422  eroveu  6423  ecopovtrn  6429  ecopovtrng  6432  th3qlem1  6434  th3qlem2  6435  th3q  6437  elpm2r  6463  mapsncnv  6492  elixp2  6499  ixpeq1  6506  elixpsn  6532  ixpsnf1o  6533  mapsnen  6608  map1  6609  xpsnen  6617  endisj  6620  xpf1o  6640  phplem3g  6652  ssfiexmid  6672  domfiexmid  6674  findcard2s  6686  isinfinf  6693  ac6sfi  6694  fiintim  6719  fisseneq  6722  f1dmvrnfibi  6733  sbthlem2  6747  isbth  6756  supeq1  6761  supeq3  6765  supeq123d  6766  supmoti  6768  eqsupti  6771  supsnti  6780  isotilem  6781  isoti  6782  supisolem  6783  supisoex  6784  cnvinfex  6793  cnvti  6794  eqinfti  6795  infvalti  6797  updjud  6853  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  ltsopi  6976  recexnq  7046  recmulnqg  7047  ltsonq  7054  lt2addnq  7060  lt2mulnq  7061  ltbtwnnqq  7071  prarloclemarch2  7075  enq0sym  7088  enq0ref  7089  enq0tr  7090  enq0breq  7092  addnq0mo  7103  mulnq0mo  7104  addnnnq0  7105  mulnnnq0  7106  nqnq0a  7110  nqnq0m  7111  elinp  7130  prcdnql  7140  prcunqu  7141  prltlu  7143  prdisj  7148  prarloclemlo  7150  prarloclem3  7153  prarloclem5  7156  ltdfpr  7162  genprndl  7177  genprndu  7178  genpdisj  7179  appdivnq  7219  ltpopr  7251  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  ltexpri  7269  recexprlemm  7280  recexprlemdisj  7286  recexprlemloc  7287  recexprlem1ssl  7289  recexprlem1ssu  7290  recexpr  7294  aptiprleml  7295  archpr  7299  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  cauappcvgprlemlim  7317  cauappcvgpr  7318  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemcl  7332  caucvgpr  7338  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemopu  7355  caucvgprpr  7368  addsrmo  7386  mulsrmo  7387  addsrpr  7388  mulsrpr  7389  lttrsr  7405  recexgt0sr  7416  caucvgsrlemcau  7435  caucvgsrlemgt1  7437  caucvgsrlemoffcau  7440  caucvgsrlemoffres  7442  caucvgsr  7444  ltresr  7473  pitonn  7482  peano1nnnn  7486  peano2nnnn  7487  axprecex  7512  axcnre  7513  axpre-lttrn  7516  peano5nnnn  7524  axcaucvglemcau  7530  axcaucvglemres  7531  axlttrn  7652  letri3  7663  letr  7665  le2add  8019  lt2add  8020  ltleadd  8021  lt2sub  8035  le2sub  8036  apreap  8161  apreim  8177  apti  8196  msq11  8460  dfinfre  8514  sup3exmid  8515  cju  8519  peano5nni  8523  1nn  8531  peano2nn  8532  nn2ge  8553  nominpos  8751  elz2  8916  dfuzi  8955  uzind  8956  supinfneg  9182  infsupneg  9183  xrletri3  9371  xrletr  9374  z2ge  9392  elixx1  9463  elioo2  9487  iooshf  9518  iooneg  9554  iccneg  9555  icoshft  9556  elfz1  9578  fzdifsuc  9644  fzrev  9647  1fv  9699  exbtwnzlemstep  9808  exbtwnzlemshrink  9809  exbtwnzlemex  9810  exbtwnz  9811  rebtwn2zlemstep  9813  rebtwn2zlemshrink  9814  rebtwn2z  9815  qbtwnre  9817  qbtwnxr  9818  flval  9828  flqlelt  9832  flqbi  9846  flqbi2  9847  modqid2  9907  q2submod  9941  nnesq  10188  hashunlem  10327  zfz1isolem1  10360  zfz1iso  10361  seq3coll  10362  shftlem  10365  shftfibg  10369  shftfib  10372  shftfn  10373  2shfti  10380  cjval  10394  cjth  10395  remim  10409  caucvgrelemcau  10528  caucvgre  10529  cvg1nlemcau  10532  cvg1nlemres  10533  rexanuz2  10539  recvguniq  10543  resqrexlemgt0  10568  resqrexlemoverl  10569  resqrexlemglsq  10570  resqrexlemsqa  10572  resqrexlemex  10573  rsqrmo  10575  resqrtcl  10577  rersqrtthlem  10578  absdiflt  10640  absdifle  10641  cau3lem  10662  icodiamlt  10728  maxleast  10761  negfi  10774  minmax  10776  lemininf  10780  ltmininf  10781  xrmaxlesup  10802  xrminmax  10808  xrltmininf  10813  xrlemininf  10814  iooinsup  10820  clim  10824  clim2  10826  climshftlemg  10845  addcn2  10853  climcau  10890  summodc  10926  fsum3  10930  fsum2dlemstep  10977  fisumcom2  10981  fsum00  11005  sin01bnd  11197  cos01bnd  11198  divalgmod  11354  ndvdssub  11357  zsupcllemstep  11368  infssuzex  11372  gcdsupex  11376  gcdsupcl  11377  gcddvds  11382  dvdslegcd  11383  bezoutlemmain  11414  bezoutlemex  11417  bezoutlemzz  11418  bezoutlemeu  11423  bezoutlemle  11424  bezoutlemsup  11425  dfgcd3  11426  dfgcd2  11430  gcddiv  11435  lcmval  11472  lcmcllem  11476  dvdslcm  11478  lcmledvds  11479  lcmgcdlem  11486  lcmdvds  11488  coprmgcdb  11497  ncoprmgcdne1b  11498  coprmdvds1  11500  qredeu  11506  divgcdcoprm0  11510  divgcdcoprmex  11511  isprm3  11527  pw2dvdslemn  11570  pw2dvdseu  11573  oddpwdclemxy  11574  qnumdencl  11592  qnumdenbi  11597  crth  11627  istopg  11850  fiinbas  11899  eltg2  11905  topbas  11919  neiint  11997  neipsm  12006  opnneissb  12007  opnssneib  12008  innei  12015  restbasg  12020  iscnp4  12069  cnpnei  12070  cnconst2  12084  cnptopresti  12089  cnptoprest  12090  cnpdis  12093  lmss  12097  lmres  12099  ispsmet  12109  ismet  12130  isxmet  12131  bldisj  12187  blininf  12210  blssexps  12215  blssex  12216  ssblex  12217  xmspropd  12263  mspropd  12264  neibl  12277  metequiv  12281  bdmopn  12290  metrest  12292  metcnp3  12293  tgioo  12320  tgqioo  12321  mulcncflem  12353  bj-sseq  12400  bj-nalset  12494  bj-indeq  12532  bj-2inf  12541  exmidsbthrlem  12617  qdencn  12620