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  954  3anbi123d  1322  xorbi2d  1390  xorbi1d  1391  drsb1  1809  mopick  2114  clelab  2313  cbvrexfw  2706  cbvrexf  2708  cbvreu  2713  cbvrexvw  2720  cbvreuvw  2721  cbvrexdva2  2723  cbvrab  2747  gencbvex  2795  rspce  2848  eqvincf  2874  ceqsrexv  2879  elrabf  2903  rexab2  2915  reu2  2937  reu6  2938  rmo4  2942  reu8  2945  reuind  2954  sbcan  3017  sbcang  3018  sbcabel  3056  rmob  3067  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  difjust  3142  injust  3146  eldif  3150  ssconb  3280  elin  3330  opeq1  3790  opeq2  3791  2ralunsn  3810  elunii  3826  csbunig  3829  eluniab  3833  cbvopab  4086  cbvopab1  4088  cbvopab2  4089  cbvopab1s  4090  cbvopab2v  4092  cbvmptf  4109  cbvmpt  4110  trel  4120  nalset  4145  elssabg  4160  mss  4238  exss  4239  opelopab2a  4277  poeq1  4311  pocl  4315  soeq1  4327  weeq1  4368  weeq2  4369  ordeq  4384  zfun  4446  snnex  4460  reusv3  4472  ontr2exmid  4536  regexmid  4546  onintexmid  4584  reg3exmid  4591  peano5  4609  limom  4625  nnregexmid  4632  vtoclr  4686  opeliunxp  4693  poinxp  4707  opbrop  4717  csbxpg  4719  opeliunxp2  4779  relop  4789  brcogw  4808  elrnmpt1  4890  elsnres  4956  dfres2  4971  inimasn  5058  xpcanm  5080  xpcan2m  5081  elxp4  5128  elxp5  5129  cnvsom  5184  sbcfung  5252  funopg  5262  fununi  5296  funcnvuni  5297  fneq1  5316  2elresin  5339  feq1  5360  sbcfng  5375  sbcfg  5376  f1eq1  5428  foeq1  5446  f1oeq1  5461  f1oeq2  5462  f1oeq3  5463  ffoss  5505  brprcneu  5520  fv3  5550  tz6.12f  5556  ssimaex  5590  fvopab3g  5602  fvopab3ig  5603  fvopab6  5625  fmptco  5695  elunirn  5780  f1imaeq  5789  foeqcnvco  5804  fliftfun  5810  fliftval  5814  isoeq1  5815  isoeq4  5818  isoini  5832  isopolem  5836  f1oiso2  5841  riotabidv  5846  cbvriota  5854  acexmid  5887  ovanraleqv  5912  cbvoprab1  5960  cbvoprab2  5961  cbvoprab12  5962  cbvmpox  5966  ov  6008  ovig  6010  ovg  6027  caovimo  6082  caoftrn  6122  opabex3d  6136  opabex3  6137  elxp6  6184  unielxp  6189  dfoprab4  6207  dfoprab4f  6208  fmpox  6215  xporderlem  6246  poxp  6247  cnvoprab  6249  f1od2  6250  opeliunxp2f  6253  rbropapd  6257  dftpos4  6278  tpostpos  6279  smoiso  6317  tfrlem3ag  6324  tfrlem3a  6325  tfr0dm  6337  tfrlemisucaccv  6340  tfrlemiex  6346  tfrlemi1  6347  tfrlemi14d  6348  tfrexlem  6349  tfr1onlem3ag  6352  tfr1onlemsucaccv  6356  tfr1onlemex  6362  tfr1onlemaccex  6363  tfr1onlemres  6364  tfrcllemsucaccv  6369  tfrcllembxssdm  6371  tfrcllemex  6375  tfrcllemaccex  6376  tfrcllemres  6377  tfrcldm  6378  frec0g  6412  frecabcl  6414  freccllem  6417  frecfcllem  6419  frecsuclem  6421  frecsuc  6422  nnacan  6527  nnmcan  6534  nnaordex  6543  ertr  6564  brecop  6639  eroveu  6640  ecopovtrn  6646  ecopovtrng  6649  th3qlem1  6651  th3qlem2  6652  th3q  6654  elpm2r  6680  mapsncnv  6709  elixp2  6716  ixpeq1  6723  elixpsn  6749  ixpsnf1o  6750  mapsnen  6825  map1  6826  xpsnen  6835  endisj  6838  xpf1o  6858  phplem3g  6870  ssfiexmid  6890  domfiexmid  6892  findcard2s  6904  isinfinf  6911  ac6sfi  6912  fiintim  6942  fisseneq  6945  f1dmvrnfibi  6957  sbthlem2  6971  isbth  6980  supeq1  6999  supeq3  7003  supeq123d  7004  supmoti  7006  eqsupti  7009  supsnti  7018  isotilem  7019  isoti  7020  supisolem  7021  supisoex  7022  cnvinfex  7031  cnvti  7032  eqinfti  7033  infvalti  7035  updjud  7095  ctssexmid  7162  omniwomnimkv  7179  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  acfun  7220  tapeq1  7265  tapeq2  7266  exmidapne  7273  ccfunen  7277  cc2lem  7279  cc3  7281  ltsopi  7333  recexnq  7403  recmulnqg  7404  ltsonq  7411  lt2addnq  7417  lt2mulnq  7418  ltbtwnnqq  7428  prarloclemarch2  7432  enq0sym  7445  enq0ref  7446  enq0tr  7447  enq0breq  7449  addnq0mo  7460  mulnq0mo  7461  addnnnq0  7462  mulnnnq0  7463  nqnq0a  7467  nqnq0m  7468  elinp  7487  prcdnql  7497  prcunqu  7498  prltlu  7500  prdisj  7505  prarloclemlo  7507  prarloclem3  7510  prarloclem5  7513  ltdfpr  7519  genprndl  7534  genprndu  7535  genpdisj  7536  appdivnq  7576  ltpopr  7608  ltexprlemdisj  7619  ltexprlemloc  7620  ltexprlemrl  7623  ltexprlemru  7625  ltexpri  7626  recexprlemm  7637  recexprlemdisj  7643  recexprlemloc  7644  recexprlem1ssl  7646  recexprlem1ssu  7647  recexpr  7651  aptiprleml  7652  archpr  7656  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  cauappcvgprlem1  7672  cauappcvgprlemlim  7674  cauappcvgpr  7675  caucvgprlemnkj  7679  caucvgprlemnbj  7680  caucvgprlemcl  7689  caucvgpr  7695  caucvgprprlemcbv  7700  caucvgprprlemval  7701  caucvgprprlemopu  7712  caucvgprpr  7725  suplocexpr  7738  addsrmo  7756  mulsrmo  7757  addsrpr  7758  mulsrpr  7759  lttrsr  7775  recexgt0sr  7786  caucvgsrlemcau  7806  caucvgsrlemgt1  7808  caucvgsrlemoffcau  7811  caucvgsrlemoffres  7813  caucvgsr  7815  suplocsrlem  7821  ltresr  7852  pitonn  7861  peano1nnnn  7865  peano2nnnn  7866  axprecex  7893  axcnre  7894  axpre-lttrn  7897  peano5nnnn  7905  axcaucvglemcau  7911  axcaucvglemres  7912  axpre-suploclemres  7914  axpre-suploc  7915  axlttrn  8040  axsuploc  8044  letri3  8052  letr  8054  le2add  8415  lt2add  8416  ltleadd  8417  lt2sub  8431  le2sub  8432  apreap  8558  apreim  8574  apti  8593  msq11  8873  dfinfre  8927  sup3exmid  8928  cju  8932  peano5nni  8936  1nn  8944  peano2nn  8945  nn2ge  8966  nominpos  9170  elz2  9338  dfuzi  9377  uzind  9378  supinfneg  9609  infsupneg  9610  elpqb  9663  xrletri3  9818  xrletr  9822  z2ge  9840  elixx1  9911  elioo2  9935  iooshf  9966  iooneg  10002  iccneg  10003  icoshft  10004  elfz1  10027  fzdifsuc  10095  fzrev  10098  1fv  10153  exbtwnzlemstep  10262  exbtwnzlemshrink  10263  exbtwnzlemex  10264  exbtwnz  10265  rebtwn2zlemstep  10267  rebtwn2zlemshrink  10268  rebtwn2z  10269  qbtwnre  10271  qbtwnxr  10272  flval  10286  flqlelt  10290  flqbi  10304  flqbi2  10305  modqid2  10365  q2submod  10399  nnesq  10654  hashunlem  10798  zfz1isolem1  10834  zfz1iso  10835  seq3coll  10836  shftlem  10839  shftfibg  10843  shftfib  10846  shftfn  10847  2shfti  10854  cjval  10868  cjth  10869  remim  10883  caucvgrelemcau  11003  caucvgre  11004  cvg1nlemcau  11007  cvg1nlemres  11008  rexanuz2  11014  recvguniq  11018  resqrexlemgt0  11043  resqrexlemoverl  11044  resqrexlemglsq  11045  resqrexlemsqa  11047  resqrexlemex  11048  rsqrmo  11050  resqrtcl  11052  rersqrtthlem  11053  absdiflt  11115  absdifle  11116  cau3lem  11137  icodiamlt  11203  maxleast  11236  negfi  11250  minmax  11252  lemininf  11256  ltmininf  11257  xrmaxlesup  11281  xrminmax  11287  xrltmininf  11292  xrlemininf  11293  iooinsup  11299  clim  11303  clim2  11305  climshftlemg  11324  addcn2  11332  climcau  11369  summodc  11405  fsum3  11409  fsum2dlemstep  11456  fisumcom2  11460  fsum00  11484  ntrivcvgap0  11571  prodeq1f  11574  prodeq2w  11578  prodeq2  11579  prodmodc  11600  zproddc  11601  fprodseq  11605  fprodntrivap  11606  fprod2dlemstep  11644  fprodcom2fi  11648  sin01bnd  11779  cos01bnd  11780  divalgmod  11946  ndvdssub  11949  zsupcllemstep  11960  infssuzex  11964  nninfdcex  11968  zsupssdc  11969  gcdsupex  11972  gcdsupcl  11973  gcddvds  11978  dvdslegcd  11979  bezoutlemmain  12013  bezoutlemex  12016  bezoutlemzz  12017  bezoutlemeu  12022  bezoutlemle  12023  bezoutlemsup  12024  dfgcd3  12025  dfgcd2  12029  gcddiv  12034  lcmval  12077  lcmcllem  12081  dvdslcm  12083  lcmledvds  12084  lcmgcdlem  12091  lcmdvds  12093  coprmgcdb  12102  ncoprmgcdne1b  12103  coprmdvds1  12105  qredeu  12111  divgcdcoprm0  12115  divgcdcoprmex  12116  isprm3  12132  pw2dvdslemn  12179  pw2dvdseu  12182  oddpwdclemxy  12183  qnumdencl  12201  qnumdenbi  12206  crth  12238  reumodprminv  12267  pythagtriplem19  12296  pceu  12309  pczpre  12311  pcdiv  12316  pc11  12344  dvdsprmpweqle  12350  prmpwdvds  12367  pockthi  12370  infpnlem2  12372  elgz  12383  ennnfonelemim  12439  exmidunben  12441  ctinfom  12443  ctiunctlemu1st  12449  ctiunctlemu2nd  12450  ctiunctlemudc  12452  ctiunctlemfo  12454  infpn2  12471  ptex  12731  f1ocpbllem  12749  ercpbl  12769  erlecpbl  12770  grpidvalg  12811  grpidpropdg  12812  mgmlrid  12817  issgrpd  12837  sgrppropd  12838  ismnddef  12841  sgrpidmndm  12843  ismndd  12860  mndpropd  12863  mndinvmod  12868  mnd1  12869  ismhm  12875  mhmpropd  12879  issubm  12885  insubm  12894  grppropd  12915  dfgrp2  12924  isgrpid2  12937  isgrpinv  12951  grplrinv  12954  grpidinv2  12955  grpidinv  12956  dfgrp3mlem  12995  grplactcnv  12999  releqgg  13112  eqgex  13113  eqgfval  13114  eqgval  13115  cmnpropd  13132  ablpropd  13133  imasabl  13171  isrng  13186  rngdi  13192  rngdir  13193  rngpropd  13207  dfur2g  13214  issrg  13217  srgideu  13224  srgidmlem  13230  issrgid  13233  srg1zr  13239  isring  13252  ringideu  13269  ringidmlem  13274  isringid  13277  ringid  13278  ringpropd  13290  ring1  13309  oppr0g  13329  oppr1g  13330  reldvdsrsrg  13340  dvdsrvald  13341  dvdsrd  13342  dvdsrtr  13349  unitgrp  13364  dvdsrpropdg  13395  unitpropdg  13396  opprsubrngg  13431  issubrg  13441  subrg1  13451  subrgugrp  13460  subrgpropd  13468  aprval  13471  aprap  13475  islmod  13480  lmodlema  13481  islmodd  13482  lmodfopnelem2  13514  lmodprop2d  13537  islssm  13546  islssmg  13547  rnglidlrng  13687  isridl  13692  df2idl2rng  13696  quscrng  13720  istopg  13795  fiinbas  13845  eltg2  13849  topbas  13863  neiint  13941  neipsm  13950  opnneissb  13951  opnssneib  13952  innei  13959  restbasg  13964  iscnp4  14014  cnpnei  14015  cnconst2  14029  cnptopresti  14034  cnptoprest  14035  cnpdis  14038  lmss  14042  lmres  14044  txbas  14054  eltx  14055  neitx  14064  txcnp  14067  txcnmpt  14069  uptx  14070  txdis  14073  txdis1cn  14074  txlm  14075  txhmeo  14115  ispsmet  14119  ismet  14140  isxmet  14141  bldisj  14197  blininf  14220  blssexps  14225  blssex  14226  ssblex  14227  xmspropd  14273  mspropd  14274  neibl  14287  metequiv  14291  bdmopn  14300  metrest  14302  xmetxp  14303  xmetxpbl  14304  xmettx  14306  metcnp3  14307  tgioo  14342  tgqioo  14343  addcncntoplem  14347  mulcncflem  14386  dedekindeu  14397  dedekindicclemicc  14406  limccl  14424  ellimc3apf  14425  limcimolemlt  14429  limccoap  14443  sin0pilem2  14499  sincosq1sgn  14543  sincosq2sgn  14544  sincosq3sgn  14545  sincosq4sgn  14546  lgsval  14701  lgsdir2lem5  14729  lgsne0  14735  2sqlem8a  14765  2sqlem8  14766  2sqlem9  14767  bj-sseq  14840  bj-charfunbi  14859  bj-nalset  14943  bj-indeq  14977  bj-2inf  14986  strcoll2  15031  strcollnft  15032  strcollnfALT  15034  sscoll2  15036  subctctexmid  15047  exmidsbthrlem  15067  sbthom  15071  qdencn  15072  ltlenmkv  15115