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  607  pm5.17dc  909  orbididc  959  ifpbi123d  998  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  drsb1  1845  mopick  2156  clelab  2355  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrexvw  2770  cbvreuvw  2771  cbvrexdva2  2773  cbvrab  2797  gencbvex  2847  rspce  2902  eqvincf  2928  ceqsrexv  2933  elrabf  2957  rexab2  2969  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  sbcan  3071  sbcang  3072  reu8nf  3110  sbcabel  3111  rmob  3122  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  difjust  3198  injust  3202  eldif  3206  ssconb  3337  elin  3387  opeq1  3857  opeq2  3858  2ralunsn  3877  elunii  3893  csbunig  3896  eluniab  3900  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  cbvmptf  4178  cbvmpt  4179  trel  4189  nalset  4214  elssabg  4232  mss  4312  exss  4313  opelopab2a  4353  poeq1  4390  pocl  4394  soeq1  4406  weeq1  4447  weeq2  4448  ordeq  4463  zfun  4525  snnex  4539  reusv3  4551  ontr2exmid  4617  regexmid  4627  onintexmid  4665  reg3exmid  4672  peano5  4690  limom  4706  nnregexmid  4713  vtoclr  4767  opeliunxp  4774  poinxp  4788  opbrop  4798  csbxpg  4800  opeliunxp2  4862  relop  4872  brcogw  4891  elrnmpt1  4975  elsnres  5042  dfres2  5057  inimasn  5146  xpcanm  5168  xpcan2m  5169  elxp4  5216  elxp5  5217  cnvsom  5272  sbcfung  5342  funopg  5352  fununi  5389  funcnvuni  5390  fneq1  5409  2elresin  5434  feq1  5456  sbcfng  5471  sbcfg  5472  f1eq1  5528  foeq1  5546  f1oeq1  5562  f1oeq2  5563  f1oeq3  5564  ffoss  5606  brprcneu  5622  fv3  5652  tz6.12f  5658  ssimaex  5697  fvopab3g  5709  fvopab3ig  5710  fvopab6  5733  fmptco  5803  funopsn  5819  funopdmsn  5823  elunirn  5896  f1imaeq  5905  foeqcnvco  5920  fliftfun  5926  fliftval  5930  isoeq1  5931  isoeq4  5934  isoini  5948  isopolem  5952  f1oiso2  5957  riotabidv  5962  cbvriotavw  5971  cbvriota  5972  acexmid  6006  ovanraleqv  6031  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvmpox  6088  ov  6130  ovig  6132  ovg  6150  caovimo  6205  caoftrn  6257  opabex3d  6272  opabex3  6273  uchoice  6289  elxp6  6321  unielxp  6326  dfoprab4  6344  dfoprab4f  6345  fmpox  6352  xporderlem  6383  poxp  6384  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  rbropapd  6394  dftpos4  6415  tpostpos  6416  smoiso  6454  tfrlem3ag  6461  tfrlem3a  6462  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemiex  6483  tfrlemi1  6484  tfrlemi14d  6485  tfrexlem  6486  tfr1onlem3ag  6489  tfr1onlemsucaccv  6493  tfr1onlemex  6499  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnacan  6666  nnmcan  6673  nnaordex  6682  ertr  6703  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3qlem2  6793  th3q  6795  elpm2r  6821  mapsncnv  6850  elixp2  6857  ixpeq1  6864  elixpsn  6890  ixpsnf1o  6891  mapsnen  6972  map1  6973  xpsnen  6988  endisj  6991  pw2f1odclem  7003  xpf1o  7013  phplem3g  7025  ssfiexmid  7046  domfiexmid  7048  findcard2s  7060  isinfinf  7067  ac6sfi  7068  fiintim  7104  fisseneq  7107  opabfi  7111  f1dmvrnfibi  7122  sbthlem2  7136  isbth  7145  supeq1  7164  supeq3  7168  supeq123d  7169  supmoti  7171  eqsupti  7174  supsnti  7183  isotilem  7184  isoti  7185  supisolem  7186  supisoex  7187  cnvinfex  7196  cnvti  7197  eqinfti  7198  infvalti  7200  updjud  7260  ctssexmid  7328  omniwomnimkv  7345  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acneq  7395  acfun  7400  tapeq1  7449  tapeq2  7450  exmidapne  7457  ccfunen  7461  cc2lem  7463  cc3  7465  ltsopi  7518  recexnq  7588  recmulnqg  7589  ltsonq  7596  lt2addnq  7602  lt2mulnq  7603  ltbtwnnqq  7613  prarloclemarch2  7617  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  nqnq0a  7652  nqnq0m  7653  elinp  7672  prcdnql  7682  prcunqu  7683  prltlu  7685  prdisj  7690  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  ltdfpr  7704  genprndl  7719  genprndu  7720  genpdisj  7721  appdivnq  7761  ltpopr  7793  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  ltexpri  7811  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  aptiprleml  7837  archpr  7841  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgpr  7880  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemopu  7897  caucvgprpr  7910  suplocexpr  7923  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  recexgt0sr  7971  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  suplocsrlem  8006  ltresr  8037  pitonn  8046  peano1nnnn  8050  peano2nnnn  8051  axprecex  8078  axcnre  8079  axpre-lttrn  8082  peano5nnnn  8090  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  axlttrn  8226  axsuploc  8230  letri3  8238  letr  8240  le2add  8602  lt2add  8603  ltleadd  8604  lt2sub  8618  le2sub  8619  apreap  8745  apreim  8761  apti  8780  msq11  9060  dfinfre  9114  sup3exmid  9115  cju  9119  peano5nni  9124  1nn  9132  peano2nn  9133  nn2ge  9154  nominpos  9360  elz2  9529  dfuzi  9568  uzind  9569  supinfneg  9802  infsupneg  9803  elpqb  9857  xrletri3  10012  xrletr  10016  z2ge  10034  elixx1  10105  elioo2  10129  iooshf  10160  iooneg  10196  iccneg  10197  icoshft  10198  elfz1  10221  fzdifsuc  10289  fzrev  10292  1fv  10347  zsupcllemstep  10461  infssuzex  10465  nninfdcex  10469  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemshrink  10480  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2zlemshrink  10485  rebtwn2z  10486  qbtwnre  10488  qbtwnxr  10489  flval  10504  flqlelt  10508  flqbi  10522  flqbi2  10523  modqid2  10585  q2submod  10619  seqf1og  10755  nnesq  10893  hashunlem  11038  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  fundm2domnop0  11080  pfxsuffeqwrdeq  11245  swrdpfx  11254  wrd2ind  11270  swrdccatin2  11276  swrdccatin2d  11291  pfxccatin12d  11292  reuccatpfxs1lem  11293  reuccatpfxs1  11294  shftlem  11342  shftfibg  11346  shftfib  11349  shftfn  11350  2shfti  11357  cjval  11371  cjth  11372  remim  11386  caucvgrelemcau  11506  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  rexanuz2  11517  recvguniq  11521  resqrexlemgt0  11546  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  rsqrmo  11553  resqrtcl  11555  rersqrtthlem  11556  absdiflt  11618  absdifle  11619  cau3lem  11640  icodiamlt  11706  maxleast  11739  negfi  11754  minmax  11756  lemininf  11760  ltmininf  11761  xrmaxlesup  11785  xrminmax  11791  xrltmininf  11796  xrlemininf  11797  iooinsup  11803  clim  11807  clim2  11809  climshftlemg  11828  addcn2  11836  climcau  11873  summodc  11909  fsum3  11913  fsum2dlemstep  11960  fisumcom2  11964  fsum00  11988  ntrivcvgap0  12075  prodeq1f  12078  prodeq2w  12082  prodeq2  12083  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodntrivap  12110  fprod2dlemstep  12148  fprodcom2fi  12152  sin01bnd  12283  cos01bnd  12284  divalgmod  12453  ndvdssub  12456  gcdsupex  12493  gcdsupcl  12494  gcddvds  12499  dvdslegcd  12500  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemzz  12538  bezoutlemeu  12543  bezoutlemle  12544  bezoutlemsup  12545  dfgcd3  12546  dfgcd2  12550  gcddiv  12555  lcmval  12600  lcmcllem  12604  dvdslcm  12606  lcmledvds  12607  lcmgcdlem  12614  lcmdvds  12616  coprmgcdb  12625  ncoprmgcdne1b  12626  coprmdvds1  12628  qredeu  12634  divgcdcoprm0  12638  divgcdcoprmex  12639  isprm3  12655  pw2dvdslemn  12702  pw2dvdseu  12705  oddpwdclemxy  12706  qnumdencl  12724  qnumdenbi  12729  crth  12761  reumodprminv  12791  pythagtriplem19  12820  pceu  12833  pczpre  12835  pcdiv  12840  pc11  12869  dvdsprmpweqle  12875  prmpwdvds  12893  pockthi  12896  infpnlem2  12898  elgz  12909  4sqlem12  12940  ennnfonelemim  13010  exmidunben  13012  ctinfom  13014  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  ctiunctlemudc  13023  ctiunctlemfo  13025  infpn2  13042  ptex  13312  prdsval  13321  f1ocpbllem  13358  ercpbl  13379  erlecpbl  13380  grpidvalg  13421  grpidpropdg  13422  mgmlrid  13427  igsumvalx  13437  gsumfzval  13439  gsumress  13443  gsumval2  13445  issgrpd  13460  sgrppropd  13461  ismnddef  13466  sgrpidmndm  13468  ismndd  13485  mndpropd  13488  mndinvmod  13493  mnd1  13503  ismhm  13509  mhmex  13510  mhmpropd  13514  issubm  13520  insubm  13533  grppropd  13565  dfgrp2  13575  isgrpid2  13588  isgrpinv  13602  grplrinv  13605  grpidinv2  13606  grpidinv  13607  dfgrp3mlem  13646  grplactcnv  13650  releqgg  13772  eqgex  13773  eqgfval  13774  eqgval  13775  isghm  13795  ghmrn  13809  resghm  13812  ghmpropd  13835  cmnpropd  13847  ablpropd  13848  imasabl  13888  isrng  13912  rngdi  13918  rngdir  13919  rngpropd  13933  dfur2g  13940  issrg  13943  srgideu  13950  srgidmlem  13956  issrgid  13959  srg1zr  13965  isring  13978  ringideu  13995  ringidmlem  14000  isringid  14003  ringid  14004  ringpropd  14016  ring1  14037  oppr0g  14059  oppr1g  14060  dvdsrvald  14072  dvdsrd  14073  dvdsrtr  14080  unitgrp  14095  dvdsrpropdg  14126  unitpropdg  14127  rhmopp  14155  opprnzrbg  14164  opprsubrngg  14190  issubrg  14200  subrg1  14210  subrgugrp  14219  resrhm2b  14228  subrgpropd  14232  rhmpropd  14233  opprdomnbg  14253  aprval  14261  aprap  14265  islmod  14270  lmodlema  14271  islmodd  14272  lmodfopnelem2  14304  lmodprop2d  14327  islssm  14336  islssmg  14337  rnglidlrng  14477  isridl  14483  df2idl2rng  14487  quscrng  14512  istopg  14688  fiinbas  14738  eltg2  14742  topbas  14756  neiint  14834  neipsm  14843  opnneissb  14844  opnssneib  14845  innei  14852  restbasg  14857  iscnp4  14907  cnpnei  14908  cnconst2  14922  cnptopresti  14927  cnptoprest  14928  cnpdis  14931  lmss  14935  lmres  14937  txbas  14947  eltx  14948  neitx  14957  txcnp  14960  txcnmpt  14962  uptx  14963  txdis  14966  txdis1cn  14967  txlm  14968  txhmeo  15008  ispsmet  15012  ismet  15033  isxmet  15034  bldisj  15090  blininf  15113  blssexps  15118  blssex  15119  ssblex  15120  xmspropd  15166  mspropd  15167  neibl  15180  metequiv  15184  bdmopn  15193  metrest  15195  xmetxp  15196  xmetxpbl  15197  xmettx  15199  metcnp3  15200  tgioo  15243  tgqioo  15244  addcncntoplem  15250  mpomulcn  15255  mulcncflem  15296  dedekindeu  15312  dedekindicclemicc  15321  limccl  15348  ellimc3apf  15349  limcimolemlt  15353  limccoap  15367  elply2  15424  sin0pilem2  15471  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  perfect  15690  lgsval  15698  lgsdir2lem5  15726  lgsne0  15732  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad  15774  2lgslem3  15795  2sqlem8a  15816  2sqlem8  15817  2sqlem9  15818  gropd  15863  grstructd2dom  15864  incistruhgr  15905  uhgr2edg  16019  wlkeq  16095  istrl  16124  bj-sseq  16211  bj-charfunbi  16229  bj-nalset  16313  bj-indeq  16347  bj-2inf  16356  strcoll2  16401  strcollnft  16402  strcollnfALT  16404  sscoll2  16406  subctctexmid  16425  domomsubct  16426  exmidsbthrlem  16450  sbthom  16454  qdencn  16455  ltlenmkv  16498