Theorem anbi12d 477

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 469	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 468	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 188	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:  pm4.38  613  pm5.17dc  916  orbididc  966  ifpbi123d  1005  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  drsb1  1852  mopick  2165  clelab  2366  cbvrmow  2735  cbvrexfw  2776  cbvrexf  2778  cbvreu  2784  cbvrexvw  2791  cbvreuvw  2792  cbvrexdva2  2794  cbvrab  2819  gencbvex  2869  rspce  2924  eqvincf  2951  ceqsrexv  2956  elrabf  2980  rexab2  2992  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  sbcan  3094  sbcang  3095  reu8nf  3133  sbcabel  3134  rmob  3145  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  difjust  3221  injust  3225  eldif  3229  ssconb  3362  elin  3412  opeq1  3904  opeq2  3905  2ralunsn  3924  elunii  3940  csbunig  3943  eluniab  3947  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  cbvmptf  4225  cbvmpt  4226  trel  4236  nalset  4263  elssabg  4284  mss  4366  exss  4367  opelopab2a  4407  poeq1  4444  pocl  4448  soeq1  4460  weeq1  4501  weeq2  4502  ordeq  4517  zfun  4579  snnex  4594  reusv3  4606  ontr2exmid  4672  regexmid  4682  onintexmid  4720  reg3exmid  4727  peano5  4745  limom  4761  nnregexmid  4768  vtoclr  4823  opeliunxp  4830  poinxp  4844  opbrop  4854  csbxpg  4856  opeliunxp2  4920  relop  4930  brcogw  4949  elrnmpt1  5033  elsnres  5100  dfres2  5115  inimasn  5205  xpcanm  5227  xpcan2m  5228  elxp4  5275  elxp5  5276  cnvsom  5331  sbcfung  5401  funopg  5411  fununi  5449  funcnvuni  5450  fneq1  5469  2elresin  5494  feq1  5516  sbcfng  5531  sbcfg  5532  f1eq1  5593  foeq1  5611  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  ffoss  5672  brprcneu  5688  fv3  5718  tz6.12f  5724  ssimaex  5764  fvopab3g  5778  fvopab3ig  5779  fvopab6  5805  fmptco  5874  fsn2g  5883  funopsn  5891  funopdmsn  5895  elunirn  5972  f1imaeq  5981  foeqcnvco  5996  fliftfun  6002  fliftval  6006  isoeq1  6007  isoeq4  6010  isoini  6024  isopolem  6028  f1oiso2  6033  riotabidv  6040  cbvriotavw  6049  cbvriota  6050  acexmid  6084  ovanraleqv  6109  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  ov  6208  ovig  6210  ovg  6228  caovimo  6283  caoftrn  6335  opabex3d  6350  opabex3  6351  uchoice  6371  elxp6  6403  unielxp  6408  dfoprab4  6426  dfoprab4f  6427  fmpox  6436  xporderlem  6467  poxp  6468  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  rbropapd  6513  dftpos4  6534  tpostpos  6535  smoiso  6573  tfrlem3ag  6580  tfrlem3a  6581  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemiex  6602  tfrlemi1  6603  tfrlemi14d  6604  tfrexlem  6605  tfr1onlem3ag  6608  tfr1onlemsucaccv  6612  tfr1onlemex  6618  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnacan  6785  nnmcan  6792  nnaordex  6801  ertr  6822  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  th3q  6914  elpm2r  6940  mapsncnv  6977  elixp2  6984  ixpeq1  6991  elixpsn  7017  ixpsnf1o  7018  mapsnend  7099  mapsnen  7100  map1  7101  xpsnen  7119  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapunen  7151  phplem3g  7157  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard2s  7194  isinfinf  7201  ac6sfi  7202  fiintim  7238  fisseneq  7242  opabfi  7247  f1dmvrnfibi  7258  sbthlem2  7275  isbth  7284  isfsupp  7289  supeq1  7326  supeq3  7330  supeq123d  7331  supmoti  7333  eqsupti  7336  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cnvinfex  7358  cnvti  7359  eqinfti  7360  infvalti  7362  updjud  7422  ctssexmid  7490  omniwomnimkv  7507  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acneq  7558  acfun  7563  papeq1  7609  papeq2  7610  tapeq1  7618  tapeq2  7619  exmidapne  7626  ccfunen  7630  cc2lem  7632  cc3  7634  ltsopi  7687  recexnq  7757  recmulnqg  7758  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  ltbtwnnqq  7782  prarloclemarch2  7786  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  nqnq0a  7821  nqnq0m  7822  elinp  7841  prcdnql  7851  prcunqu  7852  prltlu  7854  prdisj  7859  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  ltdfpr  7873  genprndl  7888  genprndu  7889  genpdisj  7890  appdivnq  7930  ltpopr  7962  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  ltexpri  7980  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  aptiprleml  8006  archpr  8010  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgpr  8049  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemopu  8066  caucvgprpr  8079  suplocexpr  8092  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  recexgt0sr  8140  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlem  8175  ltresr  8206  pitonn  8215  peano1nnnn  8219  peano2nnnn  8220  axprecex  8247  axcnre  8248  axpre-lttrn  8251  peano5nnnn  8259  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  axlttrn  8394  axsuploc  8398  letri3  8406  letr  8408  le2add  8773  lt2add  8774  ltleadd  8775  lt2sub  8789  le2sub  8790  apreap  8917  apreim  8933  apti  8952  msq11  9234  dfinfre  9288  sup3exmid  9289  cju  9293  peano5nni  9309  1nn  9317  peano2nn  9318  nn2ge  9339  nominpos  9547  elz2  9720  dfuzi  9760  uzind  9761  supinfneg  10004  infsupneg  10005  elpqb  10060  xrletri3  10216  xrletr  10220  z2ge  10238  elixx1  10309  elioo2  10333  iooshf  10364  iooneg  10400  iccneg  10401  icoshft  10402  elfz1  10426  fzdifsuc  10498  fzrev  10501  1fv  10556  zsupcllemstep  10672  infssuzex  10676  nninfdcex  10682  zsupssdc  10683  exbtwnzlemstep  10692  exbtwnzlemshrink  10693  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2zlemshrink  10698  rebtwn2z  10699  qbtwnre  10701  qbtwnxr  10702  flval  10717  flqlelt  10722  flaplelt  10723  flqbi  10738  flqbi2  10739  modqid2  10801  q2submod  10835  seqf1og  10971  nnesq  11110  hashunlem  11258  hashfibclem  11296  hashf1lem1  11299  hashf1lem2  11300  zfz1isolem1  11306  zfz1iso  11307  seq3coll  11308  fundm2domnop0  11314  pfxsuffeqwrdeq  11484  swrdpfx  11493  wrd2ind  11509  swrdccatin2  11515  swrdccatin2d  11530  pfxccatin12d  11531  reuccatpfxs1lem  11532  reuccatpfxs1  11533  shftlem  11595  shftfibg  11599  shftfib  11602  shftfn  11603  2shfti  11610  cjval  11624  cjth  11625  remim  11639  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  rexanuz2  11771  recvguniq  11775  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  rsqrmo  11807  resqrtcl  11809  rersqrtthlem  11810  absdiflt  11873  absdifle  11874  cau3lem  11895  icodiamlt  11961  maxleast  11994  negfi  12009  minmax  12011  lemininf  12015  ltmininf  12016  xrmaxlesup  12041  xrminmax  12047  xrltmininf  12052  xrlemininf  12053  iooinsup  12059  clim  12063  clim2  12065  climshftlemg  12084  addcn2  12092  climcau  12129  summodc  12166  fsum3  12170  fsum2dlemstep  12217  fisumcom2  12221  fsum00  12245  ntrivcvgap0  12332  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  fprod2dlemstep  12405  fprodcom2fi  12409  sin01bnd  12540  cos01bnd  12541  divalgmod  12710  ndvdssub  12713  gcdsupex  12750  gcdsupcl  12751  gcddvds  12756  dvdslegcd  12757  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemeu  12800  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dfgcd2  12807  gcddiv  12812  lcmval  12857  lcmcllem  12861  dvdslcm  12863  lcmledvds  12864  lcmgcdlem  12871  lcmdvds  12873  coprmgcdb  12882  ncoprmgcdne1b  12883  coprmdvds1  12885  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  isprm3  12912  pwbdvdslemn  12960  pwbdvdseu  12963  nnmaxpwlemxy  12964  qnumdencl  12983  qnumdenbi  12988  crth  13022  reumodprminv  13052  pythagtriplem19  13081  pceu  13094  pczpre  13096  pcdiv  13101  pc11  13130  dvdsprmpweqle  13136  prmpwdvds  13154  pockthi  13157  infpnlem2  13159  elgz  13170  4sqlem12  13201  ennnfonelemim  13364  exmidunben  13366  ctinfom  13368  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  infpn2  13396  ptex  13667  f1ocpbllem  13680  ercpbl  13701  erlecpbl  13702  grpidvalg  13742  grpidpropdg  13743  mgmlrid  13748  gzsumvalx  13758  gzsumfzval  13760  gzsumress  13761  gzsumval2  13763  issgrpd  13776  sgrppropd  13777  ismnddef  13780  sgrpidmndm  13782  ismndd  13799  mndpropd  13802  mndinvmod  13807  mnd1  13811  ismhm  13817  mhmex  13818  mhmpropd  13822  issubm  13828  insubm  13841  grppropd  13871  dfgrp2  13881  isgrpid2  13894  isgrpinv  13908  grplrinv  13911  grpidinv2  13912  grpidinv  13913  dfgrp3mlem  13952  grplactcnv  13956  releqgg  14072  eqgex  14073  eqgfval  14074  eqgval  14075  isghm  14095  ghmrn  14109  resghm  14112  ghmpropd  14135  cmnpropd  14147  ablpropd  14148  imasabl  14189  gsumvalfi  14201  prdsval  14222  isrng  14282  rngdi  14288  rngdir  14289  rngpropd  14303  rng1zrlem  14307  dfur2g  14315  issrg  14318  srgideu  14325  srgidmlem  14331  issrgid  14334  isring  14353  ringideu  14370  ringidmlem  14376  isringid  14379  ringid  14380  ringpropd  14392  ring1  14413  oppr0g  14436  oppr1g  14437  dvdsrvald  14449  dvdsrd  14450  dvdsrtr  14457  unitgrp  14472  dvdsrpropdg  14503  unitpropdg  14504  rhmopp  14532  opprnzrbg  14541  opprlring  14553  opprsubrngg  14568  issubrg  14578  subrg1  14588  subrgugrp  14597  resrhm2b  14606  subrgpropd  14610  rhmpropd  14611  opprdomnbg  14632  aprval  14640  aprap  14647  aprprop  14650  opprdrng  14669  islmod  14676  lmodlema  14677  islmodd  14678  lmodfopnelem2  14711  lmodprop2d  14734  islssm  14743  islssmg  14744  rnglidlrng  14884  isridl  14890  df2idl2rng  14894  quscrng  14919  isassa  15051  assalem  15052  isassad  15060  assapropd  15063  istopg  15149  fiinbas  15199  eltg2  15203  topbas  15217  neiint  15295  neipsm  15304  opnneissb  15305  opnssneib  15306  innei  15313  restbasg  15318  iscnp4  15368  cnpnei  15369  cnconst2  15383  cnptopresti  15388  cnptoprest  15389  cnpdis  15392  lmss  15396  lmres  15398  txbas  15408  eltx  15409  neitx  15418  txcnp  15421  txcnmpt  15423  uptx  15424  txdis  15427  txdis1cn  15428  txlm  15429  txhmeo  15469  ispsmet  15473  ismet  15494  isxmet  15495  bldisj  15551  blininf  15574  blssexps  15579  blssex  15580  ssblex  15581  xmspropd  15627  mspropd  15628  neibl  15641  metequiv  15645  bdmopn  15654  metrest  15656  xmetxp  15657  xmetxpbl  15658  xmettx  15660  metcnp3  15661  tgioo  15704  tgqioo  15705  addcncntoplem  15711  mpomulcn  15716  mulcncflem  15757  dedekindeu  15773  dedekindicclemicc  15782  limccl  15809  ellimc3apf  15810  limcimolemlt  15814  limccoap  15828  elply2  15885  sin0pilem2  15933  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  zprmlogbaplem3  16136  zprmlogbap  16137  pellexlem3  16150  perfect  16199  prmefexple  16206  bpos1lem  16207  bposlem1  16209  lgsval  16221  lgsdir2lem5  16249  lgsne0  16255  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad  16297  2lgslem3  16318  2sqlem8a  16339  2sqlem8  16340  2sqlem9  16341  gropd  16386  grstructd2dom  16387  incistruhgr  16429  uhgr2edg  16545  vtxd0nedgbfi  16638  wlkeq  16693  istrl  16724  clwwlkn2  16760  eupthsg  16784  iseupth  16786  eupth2lem1  16797  depind  16848  bj-sseq  16918  bj-charfunbi  16935  bj-nalset  17019  bj-indeq  17053  bj-2inf  17062  strcoll2  17107  strcollnft  17108  strcollnfALT  17110  sscoll2  17112  subctctexmid  17128  domomsubct  17129  exmidsbthrlem  17165  sbthom  17169  qdencn  17170  qdiff  17196  ltlenmkv  17218  alsbid  17241