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  605  pm5.17dc  905  orbididc  955  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  drsb1  1810  mopick  2120  clelab  2319  cbvrexfw  2717  cbvrexf  2719  cbvreu  2724  cbvrexvw  2731  cbvreuvw  2732  cbvrexdva2  2734  cbvrab  2758  gencbvex  2806  rspce  2859  eqvincf  2885  ceqsrexv  2890  elrabf  2914  rexab2  2926  reu2  2948  reu6  2949  rmo4  2953  reu8  2956  reuind  2965  sbcan  3028  sbcang  3029  sbcabel  3067  rmob  3078  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  difjust  3154  injust  3158  eldif  3162  ssconb  3292  elin  3342  opeq1  3804  opeq2  3805  2ralunsn  3824  elunii  3840  csbunig  3843  eluniab  3847  cbvopab  4100  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  cbvopab2v  4106  cbvmptf  4123  cbvmpt  4124  trel  4134  nalset  4159  elssabg  4177  mss  4255  exss  4256  opelopab2a  4295  poeq1  4330  pocl  4334  soeq1  4346  weeq1  4387  weeq2  4388  ordeq  4403  zfun  4465  snnex  4479  reusv3  4491  ontr2exmid  4557  regexmid  4567  onintexmid  4605  reg3exmid  4612  peano5  4630  limom  4646  nnregexmid  4653  vtoclr  4707  opeliunxp  4714  poinxp  4728  opbrop  4738  csbxpg  4740  opeliunxp2  4802  relop  4812  brcogw  4831  elrnmpt1  4913  elsnres  4979  dfres2  4994  inimasn  5083  xpcanm  5105  xpcan2m  5106  elxp4  5153  elxp5  5154  cnvsom  5209  sbcfung  5278  funopg  5288  fununi  5322  funcnvuni  5323  fneq1  5342  2elresin  5365  feq1  5386  sbcfng  5401  sbcfg  5402  f1eq1  5454  foeq1  5472  f1oeq1  5488  f1oeq2  5489  f1oeq3  5490  ffoss  5532  brprcneu  5547  fv3  5577  tz6.12f  5583  ssimaex  5618  fvopab3g  5630  fvopab3ig  5631  fvopab6  5654  fmptco  5724  elunirn  5809  f1imaeq  5818  foeqcnvco  5833  fliftfun  5839  fliftval  5843  isoeq1  5844  isoeq4  5847  isoini  5861  isopolem  5865  f1oiso2  5870  riotabidv  5875  cbvriota  5884  acexmid  5917  ovanraleqv  5942  cbvoprab1  5990  cbvoprab2  5991  cbvoprab12  5992  cbvmpox  5996  ov  6038  ovig  6040  ovg  6057  caovimo  6112  caoftrn  6158  opabex3d  6173  opabex3  6174  uchoice  6190  elxp6  6222  unielxp  6227  dfoprab4  6245  dfoprab4f  6246  fmpox  6253  xporderlem  6284  poxp  6285  cnvoprab  6287  f1od2  6288  opeliunxp2f  6291  rbropapd  6295  dftpos4  6316  tpostpos  6317  smoiso  6355  tfrlem3ag  6362  tfrlem3a  6363  tfr0dm  6375  tfrlemisucaccv  6378  tfrlemiex  6384  tfrlemi1  6385  tfrlemi14d  6386  tfrexlem  6387  tfr1onlem3ag  6390  tfr1onlemsucaccv  6394  tfr1onlemex  6400  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemex  6413  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  frec0g  6450  frecabcl  6452  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  nnacan  6565  nnmcan  6572  nnaordex  6581  ertr  6602  brecop  6679  eroveu  6680  ecopovtrn  6686  ecopovtrng  6689  th3qlem1  6691  th3qlem2  6692  th3q  6694  elpm2r  6720  mapsncnv  6749  elixp2  6756  ixpeq1  6763  elixpsn  6789  ixpsnf1o  6790  mapsnen  6865  map1  6866  xpsnen  6875  endisj  6878  pw2f1odclem  6890  xpf1o  6900  phplem3g  6912  ssfiexmid  6932  domfiexmid  6934  findcard2s  6946  isinfinf  6953  ac6sfi  6954  fiintim  6985  fisseneq  6988  opabfi  6992  f1dmvrnfibi  7003  sbthlem2  7017  isbth  7026  supeq1  7045  supeq3  7049  supeq123d  7050  supmoti  7052  eqsupti  7055  supsnti  7064  isotilem  7065  isoti  7066  supisolem  7067  supisoex  7068  cnvinfex  7077  cnvti  7078  eqinfti  7079  infvalti  7081  updjud  7141  ctssexmid  7209  omniwomnimkv  7226  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  acfun  7267  tapeq1  7312  tapeq2  7313  exmidapne  7320  ccfunen  7324  cc2lem  7326  cc3  7328  ltsopi  7380  recexnq  7450  recmulnqg  7451  ltsonq  7458  lt2addnq  7464  lt2mulnq  7465  ltbtwnnqq  7475  prarloclemarch2  7479  enq0sym  7492  enq0ref  7493  enq0tr  7494  enq0breq  7496  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  mulnnnq0  7510  nqnq0a  7514  nqnq0m  7515  elinp  7534  prcdnql  7544  prcunqu  7545  prltlu  7547  prdisj  7552  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  ltdfpr  7566  genprndl  7581  genprndu  7582  genpdisj  7583  appdivnq  7623  ltpopr  7655  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  ltexpri  7673  recexprlemm  7684  recexprlemdisj  7690  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  recexpr  7698  aptiprleml  7699  archpr  7703  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemcl  7736  caucvgpr  7742  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemopu  7759  caucvgprpr  7772  suplocexpr  7785  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  lttrsr  7822  recexgt0sr  7833  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  caucvgsr  7862  suplocsrlem  7868  ltresr  7899  pitonn  7908  peano1nnnn  7912  peano2nnnn  7913  axprecex  7940  axcnre  7941  axpre-lttrn  7944  peano5nnnn  7952  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  axlttrn  8088  axsuploc  8092  letri3  8100  letr  8102  le2add  8463  lt2add  8464  ltleadd  8465  lt2sub  8479  le2sub  8480  apreap  8606  apreim  8622  apti  8641  msq11  8921  dfinfre  8975  sup3exmid  8976  cju  8980  peano5nni  8985  1nn  8993  peano2nn  8994  nn2ge  9015  nominpos  9220  elz2  9388  dfuzi  9427  uzind  9428  supinfneg  9660  infsupneg  9661  elpqb  9715  xrletri3  9870  xrletr  9874  z2ge  9892  elixx1  9963  elioo2  9987  iooshf  10018  iooneg  10054  iccneg  10055  icoshft  10056  elfz1  10079  fzdifsuc  10147  fzrev  10150  1fv  10205  exbtwnzlemstep  10316  exbtwnzlemshrink  10317  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2zlemshrink  10322  rebtwn2z  10323  qbtwnre  10325  qbtwnxr  10326  flval  10341  flqlelt  10345  flqbi  10359  flqbi2  10360  modqid2  10422  q2submod  10456  seqf1og  10592  nnesq  10730  hashunlem  10875  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  shftlem  10960  shftfibg  10964  shftfib  10967  shftfn  10968  2shfti  10975  cjval  10989  cjth  10990  remim  11004  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  rexanuz2  11135  recvguniq  11139  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  rsqrmo  11171  resqrtcl  11173  rersqrtthlem  11174  absdiflt  11236  absdifle  11237  cau3lem  11258  icodiamlt  11324  maxleast  11357  negfi  11371  minmax  11373  lemininf  11377  ltmininf  11378  xrmaxlesup  11402  xrminmax  11408  xrltmininf  11413  xrlemininf  11414  iooinsup  11420  clim  11424  clim2  11426  climshftlemg  11445  addcn2  11453  climcau  11490  summodc  11526  fsum3  11530  fsum2dlemstep  11577  fisumcom2  11581  fsum00  11605  ntrivcvgap0  11692  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  fprod2dlemstep  11765  fprodcom2fi  11769  sin01bnd  11900  cos01bnd  11901  divalgmod  12068  ndvdssub  12071  zsupcllemstep  12082  infssuzex  12086  nninfdcex  12090  zsupssdc  12091  gcdsupex  12094  gcdsupcl  12095  gcddvds  12100  dvdslegcd  12101  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemeu  12144  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dfgcd2  12151  gcddiv  12156  lcmval  12201  lcmcllem  12205  dvdslcm  12207  lcmledvds  12208  lcmgcdlem  12215  lcmdvds  12217  coprmgcdb  12226  ncoprmgcdne1b  12227  coprmdvds1  12229  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  isprm3  12256  pw2dvdslemn  12303  pw2dvdseu  12306  oddpwdclemxy  12307  qnumdencl  12325  qnumdenbi  12330  crth  12362  reumodprminv  12391  pythagtriplem19  12420  pceu  12433  pczpre  12435  pcdiv  12440  pc11  12469  dvdsprmpweqle  12475  prmpwdvds  12493  pockthi  12496  infpnlem2  12498  elgz  12509  4sqlem12  12540  ennnfonelemim  12581  exmidunben  12583  ctinfom  12585  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunctlemfo  12596  infpn2  12613  ptex  12875  f1ocpbllem  12893  ercpbl  12914  erlecpbl  12915  grpidvalg  12956  grpidpropdg  12957  mgmlrid  12962  igsumvalx  12972  gsumfzval  12974  gsumress  12978  gsumval2  12980  issgrpd  12995  sgrppropd  12996  ismnddef  12999  sgrpidmndm  13001  ismndd  13018  mndpropd  13021  mndinvmod  13026  mnd1  13027  ismhm  13033  mhmex  13034  mhmpropd  13038  issubm  13044  insubm  13057  grppropd  13089  dfgrp2  13099  isgrpid2  13112  isgrpinv  13126  grplrinv  13129  grpidinv2  13130  grpidinv  13131  dfgrp3mlem  13170  grplactcnv  13174  releqgg  13290  eqgex  13291  eqgfval  13292  eqgval  13293  isghm  13313  ghmrn  13327  resghm  13330  ghmpropd  13353  cmnpropd  13365  ablpropd  13366  imasabl  13406  isrng  13430  rngdi  13436  rngdir  13437  rngpropd  13451  dfur2g  13458  issrg  13461  srgideu  13468  srgidmlem  13474  issrgid  13477  srg1zr  13483  isring  13496  ringideu  13513  ringidmlem  13518  isringid  13521  ringid  13522  ringpropd  13534  ring1  13555  oppr0g  13577  oppr1g  13578  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrd  13590  dvdsrtr  13597  unitgrp  13612  dvdsrpropdg  13643  unitpropdg  13644  rhmopp  13672  opprnzrbg  13681  opprsubrngg  13707  issubrg  13717  subrg1  13727  subrgugrp  13736  resrhm2b  13745  subrgpropd  13749  rhmpropd  13750  opprdomnbg  13770  aprval  13778  aprap  13782  islmod  13787  lmodlema  13788  islmodd  13789  lmodfopnelem2  13821  lmodprop2d  13844  islssm  13853  islssmg  13854  rnglidlrng  13994  isridl  14000  df2idl2rng  14004  quscrng  14029  istopg  14167  fiinbas  14217  eltg2  14221  topbas  14235  neiint  14313  neipsm  14322  opnneissb  14323  opnssneib  14324  innei  14331  restbasg  14336  iscnp4  14386  cnpnei  14387  cnconst2  14401  cnptopresti  14406  cnptoprest  14407  cnpdis  14410  lmss  14414  lmres  14416  txbas  14426  eltx  14427  neitx  14436  txcnp  14439  txcnmpt  14441  uptx  14442  txdis  14445  txdis1cn  14446  txlm  14447  txhmeo  14487  ispsmet  14491  ismet  14512  isxmet  14513  bldisj  14569  blininf  14592  blssexps  14597  blssex  14598  ssblex  14599  xmspropd  14645  mspropd  14646  neibl  14659  metequiv  14663  bdmopn  14672  metrest  14674  xmetxp  14675  xmetxpbl  14676  xmettx  14678  metcnp3  14679  tgioo  14714  tgqioo  14715  addcncntoplem  14719  mulcncflem  14761  dedekindeu  14777  dedekindicclemicc  14786  limccl  14813  ellimc3apf  14814  limcimolemlt  14818  limccoap  14832  elply2  14881  sin0pilem2  14917  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  lgsval  15120  lgsdir2lem5  15148  lgsne0  15154  lgsquadlem1  15191  2sqlem8a  15209  2sqlem8  15210  2sqlem9  15211  bj-sseq  15284  bj-charfunbi  15303  bj-nalset  15387  bj-indeq  15421  bj-2inf  15430  strcoll2  15475  strcollnft  15476  strcollnfALT  15478  sscoll2  15480  subctctexmid  15491  exmidsbthrlem  15512  sbthom  15516  qdencn  15517  ltlenmkv  15560