Theorem anbi12d 473

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 465	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 464	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 188	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:  pm4.38  609  pm5.17dc  911  orbididc  961  ifpbi123d  1000  3anbi123d  1348  xorbi2d  1424  xorbi1d  1425  drsb1  1847  mopick  2158  clelab  2357  cbvrmow  2716  cbvrexfw  2757  cbvrexf  2759  cbvreu  2765  cbvrexvw  2772  cbvreuvw  2773  cbvrexdva2  2775  cbvrab  2800  gencbvex  2850  rspce  2905  eqvincf  2931  ceqsrexv  2936  elrabf  2960  rexab2  2972  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  sbcan  3074  sbcang  3075  reu8nf  3113  sbcabel  3114  rmob  3125  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  difjust  3201  injust  3205  eldif  3209  ssconb  3340  elin  3390  opeq1  3862  opeq2  3863  2ralunsn  3882  elunii  3898  csbunig  3901  eluniab  3905  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  cbvmptf  4183  cbvmpt  4184  trel  4194  nalset  4219  elssabg  4238  mss  4318  exss  4319  opelopab2a  4359  poeq1  4396  pocl  4400  soeq1  4412  weeq1  4453  weeq2  4454  ordeq  4469  zfun  4531  snnex  4545  reusv3  4557  ontr2exmid  4623  regexmid  4633  onintexmid  4671  reg3exmid  4678  peano5  4696  limom  4712  nnregexmid  4719  vtoclr  4774  opeliunxp  4781  poinxp  4795  opbrop  4805  csbxpg  4807  opeliunxp2  4870  relop  4880  brcogw  4899  elrnmpt1  4983  elsnres  5050  dfres2  5065  inimasn  5154  xpcanm  5176  xpcan2m  5177  elxp4  5224  elxp5  5225  cnvsom  5280  sbcfung  5350  funopg  5360  fununi  5398  funcnvuni  5399  fneq1  5418  2elresin  5443  feq1  5465  sbcfng  5480  sbcfg  5481  f1eq1  5537  foeq1  5555  f1oeq1  5571  f1oeq2  5572  f1oeq3  5573  ffoss  5616  brprcneu  5632  fv3  5662  tz6.12f  5668  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvopab6  5743  fmptco  5813  funopsn  5829  funopdmsn  5833  elunirn  5906  f1imaeq  5915  foeqcnvco  5930  fliftfun  5936  fliftval  5940  isoeq1  5941  isoeq4  5944  isoini  5958  isopolem  5962  f1oiso2  5967  riotabidv  5972  cbvriotavw  5981  cbvriota  5982  acexmid  6016  ovanraleqv  6041  cbvoprab1  6092  cbvoprab2  6093  cbvoprab12  6094  cbvmpox  6098  ov  6140  ovig  6142  ovg  6160  caovimo  6215  caoftrn  6267  opabex3d  6282  opabex3  6283  uchoice  6299  elxp6  6331  unielxp  6336  dfoprab4  6354  dfoprab4f  6355  fmpox  6364  xporderlem  6395  poxp  6396  cnvoprab  6398  f1od2  6399  opeliunxp2f  6403  rbropapd  6407  dftpos4  6428  tpostpos  6429  smoiso  6467  tfrlem3ag  6474  tfrlem3a  6475  tfr0dm  6487  tfrlemisucaccv  6490  tfrlemiex  6496  tfrlemi1  6497  tfrlemi14d  6498  tfrexlem  6499  tfr1onlem3ag  6502  tfr1onlemsucaccv  6506  tfr1onlemex  6512  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  frec0g  6562  frecabcl  6564  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  nnacan  6679  nnmcan  6686  nnaordex  6695  ertr  6716  brecop  6793  eroveu  6794  ecopovtrn  6800  ecopovtrng  6803  th3qlem1  6805  th3qlem2  6806  th3q  6808  elpm2r  6834  mapsncnv  6863  elixp2  6870  ixpeq1  6877  elixpsn  6903  ixpsnf1o  6904  mapsnen  6985  map1  6986  xpsnen  7004  endisj  7007  pw2f1odclem  7019  xpf1o  7029  phplem3g  7041  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  findcard2s  7078  isinfinf  7085  ac6sfi  7086  fiintim  7122  fisseneq  7126  opabfi  7131  f1dmvrnfibi  7142  sbthlem2  7156  isbth  7165  supeq1  7184  supeq3  7188  supeq123d  7189  supmoti  7191  eqsupti  7194  supsnti  7203  isotilem  7204  isoti  7205  supisolem  7206  supisoex  7207  cnvinfex  7216  cnvti  7217  eqinfti  7218  infvalti  7220  updjud  7280  ctssexmid  7348  omniwomnimkv  7365  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acneq  7416  acfun  7421  tapeq1  7470  tapeq2  7471  exmidapne  7478  ccfunen  7482  cc2lem  7484  cc3  7486  ltsopi  7539  recexnq  7609  recmulnqg  7610  ltsonq  7617  lt2addnq  7623  lt2mulnq  7624  ltbtwnnqq  7634  prarloclemarch2  7638  enq0sym  7651  enq0ref  7652  enq0tr  7653  enq0breq  7655  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  nqnq0a  7673  nqnq0m  7674  elinp  7693  prcdnql  7703  prcunqu  7704  prltlu  7706  prdisj  7711  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  ltdfpr  7725  genprndl  7740  genprndu  7741  genpdisj  7742  appdivnq  7782  ltpopr  7814  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  ltexpri  7832  recexprlemm  7843  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  recexpr  7857  aptiprleml  7858  archpr  7862  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  cauappcvgpr  7881  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemcl  7895  caucvgpr  7901  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemopu  7918  caucvgprpr  7931  suplocexpr  7944  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  lttrsr  7981  recexgt0sr  7992  caucvgsrlemcau  8012  caucvgsrlemgt1  8014  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  caucvgsr  8021  suplocsrlem  8027  ltresr  8058  pitonn  8067  peano1nnnn  8071  peano2nnnn  8072  axprecex  8099  axcnre  8100  axpre-lttrn  8103  peano5nnnn  8111  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  axlttrn  8247  axsuploc  8251  letri3  8259  letr  8261  le2add  8623  lt2add  8624  ltleadd  8625  lt2sub  8639  le2sub  8640  apreap  8766  apreim  8782  apti  8801  msq11  9081  dfinfre  9135  sup3exmid  9136  cju  9140  peano5nni  9145  1nn  9153  peano2nn  9154  nn2ge  9175  nominpos  9381  elz2  9550  dfuzi  9589  uzind  9590  supinfneg  9828  infsupneg  9829  elpqb  9883  xrletri3  10038  xrletr  10042  z2ge  10060  elixx1  10131  elioo2  10155  iooshf  10186  iooneg  10222  iccneg  10223  icoshft  10224  elfz1  10247  fzdifsuc  10315  fzrev  10318  1fv  10373  zsupcllemstep  10488  infssuzex  10492  nninfdcex  10496  zsupssdc  10497  exbtwnzlemstep  10506  exbtwnzlemshrink  10507  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2zlemshrink  10512  rebtwn2z  10513  qbtwnre  10515  qbtwnxr  10516  flval  10531  flqlelt  10535  flqbi  10549  flqbi2  10550  modqid2  10612  q2submod  10646  seqf1og  10782  nnesq  10920  hashunlem  11066  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  fundm2domnop0  11108  pfxsuffeqwrdeq  11278  swrdpfx  11287  wrd2ind  11303  swrdccatin2  11309  swrdccatin2d  11324  pfxccatin12d  11325  reuccatpfxs1lem  11326  reuccatpfxs1  11327  shftlem  11376  shftfibg  11380  shftfib  11383  shftfn  11384  2shfti  11391  cjval  11405  cjth  11406  remim  11420  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  rexanuz2  11551  recvguniq  11555  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  rsqrmo  11587  resqrtcl  11589  rersqrtthlem  11590  absdiflt  11652  absdifle  11653  cau3lem  11674  icodiamlt  11740  maxleast  11773  negfi  11788  minmax  11790  lemininf  11794  ltmininf  11795  xrmaxlesup  11819  xrminmax  11825  xrltmininf  11830  xrlemininf  11831  iooinsup  11837  clim  11841  clim2  11843  climshftlemg  11862  addcn2  11870  climcau  11907  summodc  11943  fsum3  11947  fsum2dlemstep  11994  fisumcom2  11998  fsum00  12022  ntrivcvgap0  12109  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  fprod2dlemstep  12182  fprodcom2fi  12186  sin01bnd  12317  cos01bnd  12318  divalgmod  12487  ndvdssub  12490  gcdsupex  12527  gcdsupcl  12528  gcddvds  12533  dvdslegcd  12534  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemeu  12577  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  dfgcd2  12584  gcddiv  12589  lcmval  12634  lcmcllem  12638  dvdslcm  12640  lcmledvds  12641  lcmgcdlem  12648  lcmdvds  12650  coprmgcdb  12659  ncoprmgcdne1b  12660  coprmdvds1  12662  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  isprm3  12689  pw2dvdslemn  12736  pw2dvdseu  12739  oddpwdclemxy  12740  qnumdencl  12758  qnumdenbi  12763  crth  12795  reumodprminv  12825  pythagtriplem19  12854  pceu  12867  pczpre  12869  pcdiv  12874  pc11  12903  dvdsprmpweqle  12909  prmpwdvds  12927  pockthi  12930  infpnlem2  12932  elgz  12943  4sqlem12  12974  ennnfonelemim  13044  exmidunben  13046  ctinfom  13048  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunctlemfo  13059  infpn2  13076  ptex  13346  prdsval  13355  f1ocpbllem  13392  ercpbl  13413  erlecpbl  13414  grpidvalg  13455  grpidpropdg  13456  mgmlrid  13461  igsumvalx  13471  gsumfzval  13473  gsumress  13477  gsumval2  13479  issgrpd  13494  sgrppropd  13495  ismnddef  13500  sgrpidmndm  13502  ismndd  13519  mndpropd  13522  mndinvmod  13527  mnd1  13537  ismhm  13543  mhmex  13544  mhmpropd  13548  issubm  13554  insubm  13567  grppropd  13599  dfgrp2  13609  isgrpid2  13622  isgrpinv  13636  grplrinv  13639  grpidinv2  13640  grpidinv  13641  dfgrp3mlem  13680  grplactcnv  13684  releqgg  13806  eqgex  13807  eqgfval  13808  eqgval  13809  isghm  13829  ghmrn  13843  resghm  13846  ghmpropd  13869  cmnpropd  13881  ablpropd  13882  imasabl  13922  isrng  13946  rngdi  13952  rngdir  13953  rngpropd  13967  dfur2g  13974  issrg  13977  srgideu  13984  srgidmlem  13990  issrgid  13993  srg1zr  13999  isring  14012  ringideu  14029  ringidmlem  14034  isringid  14037  ringid  14038  ringpropd  14050  ring1  14071  oppr0g  14093  oppr1g  14094  dvdsrvald  14106  dvdsrd  14107  dvdsrtr  14114  unitgrp  14129  dvdsrpropdg  14160  unitpropdg  14161  rhmopp  14189  opprnzrbg  14198  opprsubrngg  14224  issubrg  14234  subrg1  14244  subrgugrp  14253  resrhm2b  14262  subrgpropd  14266  rhmpropd  14267  opprdomnbg  14287  aprval  14295  aprap  14299  islmod  14304  lmodlema  14305  islmodd  14306  lmodfopnelem2  14338  lmodprop2d  14361  islssm  14370  islssmg  14371  rnglidlrng  14511  isridl  14517  df2idl2rng  14521  quscrng  14546  istopg  14722  fiinbas  14772  eltg2  14776  topbas  14790  neiint  14868  neipsm  14877  opnneissb  14878  opnssneib  14879  innei  14886  restbasg  14891  iscnp4  14941  cnpnei  14942  cnconst2  14956  cnptopresti  14961  cnptoprest  14962  cnpdis  14965  lmss  14969  lmres  14971  txbas  14981  eltx  14982  neitx  14991  txcnp  14994  txcnmpt  14996  uptx  14997  txdis  15000  txdis1cn  15001  txlm  15002  txhmeo  15042  ispsmet  15046  ismet  15067  isxmet  15068  bldisj  15124  blininf  15147  blssexps  15152  blssex  15153  ssblex  15154  xmspropd  15200  mspropd  15201  neibl  15214  metequiv  15218  bdmopn  15227  metrest  15229  xmetxp  15230  xmetxpbl  15231  xmettx  15233  metcnp3  15234  tgioo  15277  tgqioo  15278  addcncntoplem  15284  mpomulcn  15289  mulcncflem  15330  dedekindeu  15346  dedekindicclemicc  15355  limccl  15382  ellimc3apf  15383  limcimolemlt  15387  limccoap  15401  elply2  15458  sin0pilem2  15505  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  perfect  15724  lgsval  15732  lgsdir2lem5  15760  lgsne0  15766  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad  15808  2lgslem3  15829  2sqlem8a  15850  2sqlem8  15851  2sqlem9  15852  gropd  15897  grstructd2dom  15898  incistruhgr  15940  uhgr2edg  16056  vtxd0nedgbfi  16149  wlkeq  16204  istrl  16235  clwwlkn2  16271  eupthsg  16295  iseupth  16297  eupth2lem1  16308  bj-sseq  16388  bj-charfunbi  16406  bj-nalset  16490  bj-indeq  16524  bj-2inf  16533  strcoll2  16578  strcollnft  16579  strcollnfALT  16581  sscoll2  16583  subctctexmid  16601  domomsubct  16602  exmidsbthrlem  16626  sbthom  16630  qdencn  16631  ltlenmkv  16674  gfsumval  16680