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  1813  mopick  2123  clelab  2322  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrexvw  2734  cbvreuvw  2735  cbvrexdva2  2737  cbvrab  2761  gencbvex  2810  rspce  2863  eqvincf  2889  ceqsrexv  2894  elrabf  2918  rexab2  2930  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  sbcan  3032  sbcang  3033  sbcabel  3071  rmob  3082  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  difjust  3158  injust  3162  eldif  3166  ssconb  3297  elin  3347  opeq1  3809  opeq2  3810  2ralunsn  3829  elunii  3845  csbunig  3848  eluniab  3852  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  cbvmptf  4128  cbvmpt  4129  trel  4139  nalset  4164  elssabg  4182  mss  4260  exss  4261  opelopab2a  4300  poeq1  4335  pocl  4339  soeq1  4351  weeq1  4392  weeq2  4393  ordeq  4408  zfun  4470  snnex  4484  reusv3  4496  ontr2exmid  4562  regexmid  4572  onintexmid  4610  reg3exmid  4617  peano5  4635  limom  4651  nnregexmid  4658  vtoclr  4712  opeliunxp  4719  poinxp  4733  opbrop  4743  csbxpg  4745  opeliunxp2  4807  relop  4817  brcogw  4836  elrnmpt1  4918  elsnres  4984  dfres2  4999  inimasn  5088  xpcanm  5110  xpcan2m  5111  elxp4  5158  elxp5  5159  cnvsom  5214  sbcfung  5283  funopg  5293  fununi  5327  funcnvuni  5328  fneq1  5347  2elresin  5372  feq1  5393  sbcfng  5408  sbcfg  5409  f1eq1  5461  foeq1  5479  f1oeq1  5495  f1oeq2  5496  f1oeq3  5497  ffoss  5539  brprcneu  5554  fv3  5584  tz6.12f  5590  ssimaex  5625  fvopab3g  5637  fvopab3ig  5638  fvopab6  5661  fmptco  5731  elunirn  5816  f1imaeq  5825  foeqcnvco  5840  fliftfun  5846  fliftval  5850  isoeq1  5851  isoeq4  5854  isoini  5868  isopolem  5872  f1oiso2  5877  riotabidv  5882  cbvriota  5891  acexmid  5924  ovanraleqv  5949  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvmpox  6004  ov  6046  ovig  6048  ovg  6066  caovimo  6121  caoftrn  6172  opabex3d  6187  opabex3  6188  uchoice  6204  elxp6  6236  unielxp  6241  dfoprab4  6259  dfoprab4f  6260  fmpox  6267  xporderlem  6298  poxp  6299  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  rbropapd  6309  dftpos4  6330  tpostpos  6331  smoiso  6369  tfrlem3ag  6376  tfrlem3a  6377  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemiex  6398  tfrlemi1  6399  tfrlemi14d  6400  tfrexlem  6401  tfr1onlem3ag  6404  tfr1onlemsucaccv  6408  tfr1onlemex  6414  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  frec0g  6464  frecabcl  6466  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnacan  6579  nnmcan  6586  nnaordex  6595  ertr  6616  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3qlem2  6706  th3q  6708  elpm2r  6734  mapsncnv  6763  elixp2  6770  ixpeq1  6777  elixpsn  6803  ixpsnf1o  6804  mapsnen  6879  map1  6880  xpsnen  6889  endisj  6892  pw2f1odclem  6904  xpf1o  6914  phplem3g  6926  ssfiexmid  6946  domfiexmid  6948  findcard2s  6960  isinfinf  6967  ac6sfi  6968  fiintim  7001  fisseneq  7004  opabfi  7008  f1dmvrnfibi  7019  sbthlem2  7033  isbth  7042  supeq1  7061  supeq3  7065  supeq123d  7066  supmoti  7068  eqsupti  7071  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cnvinfex  7093  cnvti  7094  eqinfti  7095  infvalti  7097  updjud  7157  ctssexmid  7225  omniwomnimkv  7242  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  acneq  7287  acfun  7292  tapeq1  7337  tapeq2  7338  exmidapne  7345  ccfunen  7349  cc2lem  7351  cc3  7353  ltsopi  7406  recexnq  7476  recmulnqg  7477  ltsonq  7484  lt2addnq  7490  lt2mulnq  7491  ltbtwnnqq  7501  prarloclemarch2  7505  enq0sym  7518  enq0ref  7519  enq0tr  7520  enq0breq  7522  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  mulnnnq0  7536  nqnq0a  7540  nqnq0m  7541  elinp  7560  prcdnql  7570  prcunqu  7571  prltlu  7573  prdisj  7578  prarloclemlo  7580  prarloclem3  7583  prarloclem5  7586  ltdfpr  7592  genprndl  7607  genprndu  7608  genpdisj  7609  appdivnq  7649  ltpopr  7681  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  ltexpri  7699  recexprlemm  7710  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  recexpr  7724  aptiprleml  7725  archpr  7729  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemcl  7762  caucvgpr  7768  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemopu  7785  caucvgprpr  7798  suplocexpr  7811  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  lttrsr  7848  recexgt0sr  7859  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  caucvgsr  7888  suplocsrlem  7894  ltresr  7925  pitonn  7934  peano1nnnn  7938  peano2nnnn  7939  axprecex  7966  axcnre  7967  axpre-lttrn  7970  peano5nnnn  7978  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  axlttrn  8114  axsuploc  8118  letri3  8126  letr  8128  le2add  8490  lt2add  8491  ltleadd  8492  lt2sub  8506  le2sub  8507  apreap  8633  apreim  8649  apti  8668  msq11  8948  dfinfre  9002  sup3exmid  9003  cju  9007  peano5nni  9012  1nn  9020  peano2nn  9021  nn2ge  9042  nominpos  9248  elz2  9416  dfuzi  9455  uzind  9456  supinfneg  9688  infsupneg  9689  elpqb  9743  xrletri3  9898  xrletr  9902  z2ge  9920  elixx1  9991  elioo2  10015  iooshf  10046  iooneg  10082  iccneg  10083  icoshft  10084  elfz1  10107  fzdifsuc  10175  fzrev  10178  1fv  10233  zsupcllemstep  10338  infssuzex  10342  nninfdcex  10346  zsupssdc  10347  exbtwnzlemstep  10356  exbtwnzlemshrink  10357  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2zlemshrink  10362  rebtwn2z  10363  qbtwnre  10365  qbtwnxr  10366  flval  10381  flqlelt  10385  flqbi  10399  flqbi2  10400  modqid2  10462  q2submod  10496  seqf1og  10632  nnesq  10770  hashunlem  10915  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  shftlem  11000  shftfibg  11004  shftfib  11007  shftfn  11008  2shfti  11015  cjval  11029  cjth  11030  remim  11044  caucvgrelemcau  11164  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  rexanuz2  11175  recvguniq  11179  resqrexlemgt0  11204  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemsqa  11208  resqrexlemex  11209  rsqrmo  11211  resqrtcl  11213  rersqrtthlem  11214  absdiflt  11276  absdifle  11277  cau3lem  11298  icodiamlt  11364  maxleast  11397  negfi  11412  minmax  11414  lemininf  11418  ltmininf  11419  xrmaxlesup  11443  xrminmax  11449  xrltmininf  11454  xrlemininf  11455  iooinsup  11461  clim  11465  clim2  11467  climshftlemg  11486  addcn2  11494  climcau  11531  summodc  11567  fsum3  11571  fsum2dlemstep  11618  fisumcom2  11622  fsum00  11646  ntrivcvgap0  11733  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  fprod2dlemstep  11806  fprodcom2fi  11810  sin01bnd  11941  cos01bnd  11942  divalgmod  12111  ndvdssub  12114  gcdsupex  12151  gcdsupcl  12152  gcddvds  12157  dvdslegcd  12158  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemeu  12201  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  dfgcd2  12208  gcddiv  12213  lcmval  12258  lcmcllem  12262  dvdslcm  12264  lcmledvds  12265  lcmgcdlem  12272  lcmdvds  12274  coprmgcdb  12283  ncoprmgcdne1b  12284  coprmdvds1  12286  qredeu  12292  divgcdcoprm0  12296  divgcdcoprmex  12297  isprm3  12313  pw2dvdslemn  12360  pw2dvdseu  12363  oddpwdclemxy  12364  qnumdencl  12382  qnumdenbi  12387  crth  12419  reumodprminv  12449  pythagtriplem19  12478  pceu  12491  pczpre  12493  pcdiv  12498  pc11  12527  dvdsprmpweqle  12533  prmpwdvds  12551  pockthi  12554  infpnlem2  12556  elgz  12567  4sqlem12  12598  ennnfonelemim  12668  exmidunben  12670  ctinfom  12672  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunctlemfo  12683  infpn2  12700  ptex  12968  prdsval  12977  f1ocpbllem  13014  ercpbl  13035  erlecpbl  13036  grpidvalg  13077  grpidpropdg  13078  mgmlrid  13083  igsumvalx  13093  gsumfzval  13095  gsumress  13099  gsumval2  13101  issgrpd  13116  sgrppropd  13117  ismnddef  13122  sgrpidmndm  13124  ismndd  13141  mndpropd  13144  mndinvmod  13149  mnd1  13159  ismhm  13165  mhmex  13166  mhmpropd  13170  issubm  13176  insubm  13189  grppropd  13221  dfgrp2  13231  isgrpid2  13244  isgrpinv  13258  grplrinv  13261  grpidinv2  13262  grpidinv  13263  dfgrp3mlem  13302  grplactcnv  13306  releqgg  13428  eqgex  13429  eqgfval  13430  eqgval  13431  isghm  13451  ghmrn  13465  resghm  13468  ghmpropd  13491  cmnpropd  13503  ablpropd  13504  imasabl  13544  isrng  13568  rngdi  13574  rngdir  13575  rngpropd  13589  dfur2g  13596  issrg  13599  srgideu  13606  srgidmlem  13612  issrgid  13615  srg1zr  13621  isring  13634  ringideu  13651  ringidmlem  13656  isringid  13659  ringid  13660  ringpropd  13672  ring1  13693  oppr0g  13715  oppr1g  13716  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrd  13728  dvdsrtr  13735  unitgrp  13750  dvdsrpropdg  13781  unitpropdg  13782  rhmopp  13810  opprnzrbg  13819  opprsubrngg  13845  issubrg  13855  subrg1  13865  subrgugrp  13874  resrhm2b  13883  subrgpropd  13887  rhmpropd  13888  opprdomnbg  13908  aprval  13916  aprap  13920  islmod  13925  lmodlema  13926  islmodd  13927  lmodfopnelem2  13959  lmodprop2d  13982  islssm  13991  islssmg  13992  rnglidlrng  14132  isridl  14138  df2idl2rng  14142  quscrng  14167  istopg  14343  fiinbas  14393  eltg2  14397  topbas  14411  neiint  14489  neipsm  14498  opnneissb  14499  opnssneib  14500  innei  14507  restbasg  14512  iscnp4  14562  cnpnei  14563  cnconst2  14577  cnptopresti  14582  cnptoprest  14583  cnpdis  14586  lmss  14590  lmres  14592  txbas  14602  eltx  14603  neitx  14612  txcnp  14615  txcnmpt  14617  uptx  14618  txdis  14621  txdis1cn  14622  txlm  14623  txhmeo  14663  ispsmet  14667  ismet  14688  isxmet  14689  bldisj  14745  blininf  14768  blssexps  14773  blssex  14774  ssblex  14775  xmspropd  14821  mspropd  14822  neibl  14835  metequiv  14839  bdmopn  14848  metrest  14850  xmetxp  14851  xmetxpbl  14852  xmettx  14854  metcnp3  14855  tgioo  14898  tgqioo  14899  addcncntoplem  14905  mpomulcn  14910  mulcncflem  14951  dedekindeu  14967  dedekindicclemicc  14976  limccl  15003  ellimc3apf  15004  limcimolemlt  15008  limccoap  15022  elply2  15079  sin0pilem2  15126  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  perfect  15345  lgsval  15353  lgsdir2lem5  15381  lgsne0  15387  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad  15429  2lgslem3  15450  2sqlem8a  15471  2sqlem8  15472  2sqlem9  15473  bj-sseq  15546  bj-charfunbi  15565  bj-nalset  15649  bj-indeq  15683  bj-2inf  15692  strcoll2  15737  strcollnft  15738  strcollnfALT  15740  sscoll2  15742  subctctexmid  15755  domomsubct  15756  exmidsbthrlem  15779  sbthom  15783  qdencn  15784  ltlenmkv  15827