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 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

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  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  3899  opeq2  3900  2ralunsn  3919  elunii  3935  csbunig  3938  eluniab  3942  cbvopab  4197  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  cbvopab2v  4203  cbvmptf  4220  cbvmpt  4221  trel  4231  nalset  4258  elssabg  4279  mss  4361  exss  4362  opelopab2a  4402  poeq1  4439  pocl  4443  soeq1  4455  weeq1  4496  weeq2  4497  ordeq  4512  zfun  4574  snnex  4589  reusv3  4601  ontr2exmid  4667  regexmid  4677  onintexmid  4715  reg3exmid  4722  peano5  4740  limom  4756  nnregexmid  4763  vtoclr  4818  opeliunxp  4825  poinxp  4839  opbrop  4849  csbxpg  4851  opeliunxp2  4915  relop  4925  brcogw  4944  elrnmpt1  5028  elsnres  5095  dfres2  5110  inimasn  5200  xpcanm  5222  xpcan2m  5223  elxp4  5270  elxp5  5271  cnvsom  5326  sbcfung  5396  funopg  5406  fununi  5444  funcnvuni  5445  fneq1  5464  2elresin  5489  feq1  5511  sbcfng  5526  sbcfg  5527  f1eq1  5588  foeq1  5606  f1oeq1  5622  f1oeq2  5623  f1oeq3  5624  ffoss  5667  brprcneu  5683  fv3  5713  tz6.12f  5719  ssimaex  5758  fvopab3g  5772  fvopab3ig  5773  fvopab6  5796  fmptco  5865  fsn2g  5874  funopsn  5882  funopdmsn  5886  elunirn  5962  f1imaeq  5971  foeqcnvco  5986  fliftfun  5992  fliftval  5996  isoeq1  5997  isoeq4  6000  isoini  6014  isopolem  6018  f1oiso2  6023  riotabidv  6030  cbvriotavw  6039  cbvriota  6040  acexmid  6074  ovanraleqv  6099  cbvoprab1  6150  cbvoprab2  6151  cbvoprab12  6152  cbvmpox  6156  ov  6198  ovig  6200  ovg  6218  caovimo  6273  caoftrn  6325  opabex3d  6340  opabex3  6341  uchoice  6361  elxp6  6393  unielxp  6398  dfoprab4  6416  dfoprab4f  6417  fmpox  6426  xporderlem  6457  poxp  6458  cnvoprab  6460  f1od2  6461  opeliunxp2f  6499  rbropapd  6503  dftpos4  6524  tpostpos  6525  smoiso  6563  tfrlem3ag  6570  tfrlem3a  6571  tfr0dm  6583  tfrlemisucaccv  6586  tfrlemiex  6592  tfrlemi1  6593  tfrlemi14d  6594  tfrexlem  6595  tfr1onlem3ag  6598  tfr1onlemsucaccv  6602  tfr1onlemex  6608  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemex  6621  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  frec0g  6658  frecabcl  6660  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  nnacan  6775  nnmcan  6782  nnaordex  6791  ertr  6812  brecop  6889  eroveu  6890  ecopovtrn  6896  ecopovtrng  6899  th3qlem1  6901  th3qlem2  6902  th3q  6904  elpm2r  6930  mapsncnv  6967  elixp2  6974  ixpeq1  6981  elixpsn  7007  ixpsnf1o  7008  mapsnend  7089  mapsnen  7090  map1  7091  xpsnen  7109  endisj  7112  pw2f1odclem  7124  xpf1o  7134  mapunen  7141  phplem3g  7147  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  findcard2s  7184  isinfinf  7191  ac6sfi  7192  fiintim  7228  fisseneq  7232  opabfi  7237  f1dmvrnfibi  7248  sbthlem2  7265  isbth  7274  isfsupp  7279  supeq1  7316  supeq3  7320  supeq123d  7321  supmoti  7323  eqsupti  7326  supsnti  7335  isotilem  7336  isoti  7337  supisolem  7338  supisoex  7339  cnvinfex  7348  cnvti  7349  eqinfti  7350  infvalti  7352  updjud  7412  ctssexmid  7480  omniwomnimkv  7497  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acneq  7548  acfun  7553  papeq1  7599  papeq2  7600  tapeq1  7608  tapeq2  7609  exmidapne  7616  ccfunen  7620  cc2lem  7622  cc3  7624  ltsopi  7677  recexnq  7747  recmulnqg  7748  ltsonq  7755  lt2addnq  7761  lt2mulnq  7762  ltbtwnnqq  7772  prarloclemarch2  7776  enq0sym  7789  enq0ref  7790  enq0tr  7791  enq0breq  7793  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  mulnnnq0  7807  nqnq0a  7811  nqnq0m  7812  elinp  7831  prcdnql  7841  prcunqu  7842  prltlu  7844  prdisj  7849  prarloclemlo  7851  prarloclem3  7854  prarloclem5  7857  ltdfpr  7863  genprndl  7878  genprndu  7879  genpdisj  7880  appdivnq  7920  ltpopr  7952  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  ltexpri  7970  recexprlemm  7981  recexprlemdisj  7987  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  recexpr  7995  aptiprleml  7996  archpr  8000  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  cauappcvgpr  8019  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemcl  8033  caucvgpr  8039  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemopu  8056  caucvgprpr  8069  suplocexpr  8082  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  lttrsr  8119  recexgt0sr  8130  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  caucvgsr  8159  suplocsrlem  8165  ltresr  8196  pitonn  8205  peano1nnnn  8209  peano2nnnn  8210  axprecex  8237  axcnre  8238  axpre-lttrn  8241  peano5nnnn  8249  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  axlttrn  8384  axsuploc  8388  letri3  8396  letr  8398  le2add  8762  lt2add  8763  ltleadd  8764  lt2sub  8778  le2sub  8779  apreap  8905  apreim  8921  apti  8940  msq11  9222  dfinfre  9276  sup3exmid  9277  cju  9281  peano5nni  9286  1nn  9294  peano2nn  9295  nn2ge  9316  nominpos  9522  elz2  9695  dfuzi  9735  uzind  9736  supinfneg  9974  infsupneg  9975  elpqb  10029  xrletri3  10185  xrletr  10189  z2ge  10207  elixx1  10278  elioo2  10302  iooshf  10333  iooneg  10369  iccneg  10370  icoshft  10371  elfz1  10395  fzdifsuc  10466  fzrev  10469  1fv  10524  zsupcllemstep  10640  infssuzex  10644  nninfdcex  10650  zsupssdc  10651  exbtwnzlemstep  10660  exbtwnzlemshrink  10661  exbtwnzlemex  10662  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2zlemshrink  10666  rebtwn2z  10667  qbtwnre  10669  qbtwnxr  10670  flval  10685  flqlelt  10689  flqbi  10703  flqbi2  10704  modqid2  10766  q2submod  10800  seqf1og  10936  nnesq  11075  hashunlem  11222  hashfibclem  11260  hashf1lem1  11263  hashf1lem2  11264  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  fundm2domnop0  11278  pfxsuffeqwrdeq  11448  swrdpfx  11457  wrd2ind  11473  swrdccatin2  11479  swrdccatin2d  11494  pfxccatin12d  11495  reuccatpfxs1lem  11496  reuccatpfxs1  11497  shftlem  11559  shftfibg  11563  shftfib  11566  shftfn  11567  2shfti  11574  cjval  11588  cjth  11589  remim  11603  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  rexanuz2  11735  recvguniq  11739  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  rsqrmo  11771  resqrtcl  11773  rersqrtthlem  11774  absdiflt  11836  absdifle  11837  cau3lem  11858  icodiamlt  11924  maxleast  11957  negfi  11972  minmax  11974  lemininf  11978  ltmininf  11979  xrmaxlesup  12003  xrminmax  12009  xrltmininf  12014  xrlemininf  12015  iooinsup  12021  clim  12025  clim2  12027  climshftlemg  12046  addcn2  12054  climcau  12091  summodc  12128  fsum3  12132  fsum2dlemstep  12179  fisumcom2  12183  fsum00  12207  ntrivcvgap0  12294  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodntrivap  12329  fprod2dlemstep  12367  fprodcom2fi  12371  sin01bnd  12502  cos01bnd  12503  divalgmod  12672  ndvdssub  12675  gcdsupex  12712  gcdsupcl  12713  gcddvds  12718  dvdslegcd  12719  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemzz  12757  bezoutlemeu  12762  bezoutlemle  12763  bezoutlemsup  12764  dfgcd3  12765  dfgcd2  12769  gcddiv  12774  lcmval  12819  lcmcllem  12823  dvdslcm  12825  lcmledvds  12826  lcmgcdlem  12833  lcmdvds  12835  coprmgcdb  12844  ncoprmgcdne1b  12845  coprmdvds1  12847  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  isprm3  12874  pw2dvdslemn  12921  pw2dvdseu  12924  oddpwdclemxy  12925  qnumdencl  12943  qnumdenbi  12948  crth  12980  reumodprminv  13010  pythagtriplem19  13039  pceu  13052  pczpre  13054  pcdiv  13059  pc11  13088  dvdsprmpweqle  13094  prmpwdvds  13112  pockthi  13115  infpnlem2  13117  elgz  13128  4sqlem12  13159  ennnfonelemim  13293  exmidunben  13295  ctinfom  13297  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunctlemfo  13308  infpn2  13325  ptex  13595  f1ocpbllem  13608  ercpbl  13629  erlecpbl  13630  grpidvalg  13670  grpidpropdg  13671  mgmlrid  13676  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsumval2  13691  issgrpd  13704  sgrppropd  13705  ismnddef  13708  sgrpidmndm  13710  ismndd  13727  mndpropd  13730  mndinvmod  13735  mnd1  13739  ismhm  13745  mhmex  13746  mhmpropd  13750  issubm  13756  insubm  13769  grppropd  13799  dfgrp2  13809  isgrpid2  13822  isgrpinv  13836  grplrinv  13839  grpidinv2  13840  grpidinv  13841  dfgrp3mlem  13880  grplactcnv  13884  releqgg  14000  eqgex  14001  eqgfval  14002  eqgval  14003  isghm  14023  ghmrn  14037  resghm  14040  ghmpropd  14063  cmnpropd  14075  ablpropd  14076  imasabl  14117  gsumvalfi  14129  prdsval  14150  isrng  14208  rngdi  14214  rngdir  14215  rngpropd  14229  rng1zrlem  14233  dfur2g  14240  issrg  14243  srgideu  14250  srgidmlem  14256  issrgid  14259  isring  14278  ringideu  14295  ringidmlem  14300  isringid  14303  ringid  14304  ringpropd  14316  ring1  14337  oppr0g  14360  oppr1g  14361  dvdsrvald  14373  dvdsrd  14374  dvdsrtr  14381  unitgrp  14396  dvdsrpropdg  14427  unitpropdg  14428  rhmopp  14456  opprnzrbg  14465  opprlring  14477  opprsubrngg  14492  issubrg  14502  subrg1  14512  subrgugrp  14521  resrhm2b  14530  subrgpropd  14534  rhmpropd  14535  opprdomnbg  14556  aprval  14564  aprap  14571  aprprop  14574  opprdrng  14593  islmod  14600  lmodlema  14601  islmodd  14602  lmodfopnelem2  14634  lmodprop2d  14657  islssm  14666  islssmg  14667  rnglidlrng  14807  isridl  14813  df2idl2rng  14817  quscrng  14842  istopg  15023  fiinbas  15073  eltg2  15077  topbas  15091  neiint  15169  neipsm  15178  opnneissb  15179  opnssneib  15180  innei  15187  restbasg  15192  iscnp4  15242  cnpnei  15243  cnconst2  15257  cnptopresti  15262  cnptoprest  15263  cnpdis  15266  lmss  15270  lmres  15272  txbas  15282  eltx  15283  neitx  15292  txcnp  15295  txcnmpt  15297  uptx  15298  txdis  15301  txdis1cn  15302  txlm  15303  txhmeo  15343  ispsmet  15347  ismet  15368  isxmet  15369  bldisj  15425  blininf  15448  blssexps  15453  blssex  15454  ssblex  15455  xmspropd  15501  mspropd  15502  neibl  15515  metequiv  15519  bdmopn  15528  metrest  15530  xmetxp  15531  xmetxpbl  15532  xmettx  15534  metcnp3  15535  tgioo  15578  tgqioo  15579  addcncntoplem  15585  mpomulcn  15590  mulcncflem  15631  dedekindeu  15647  dedekindicclemicc  15656  limccl  15683  ellimc3apf  15684  limcimolemlt  15688  limccoap  15702  elply2  15759  sin0pilem2  15806  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  pellexlem3  16007  perfect  16029  lgsval  16037  lgsdir2lem5  16065  lgsne0  16071  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad  16113  2lgslem3  16134  2sqlem8a  16155  2sqlem8  16156  2sqlem9  16157  gropd  16202  grstructd2dom  16203  incistruhgr  16245  uhgr2edg  16361  vtxd0nedgbfi  16454  wlkeq  16509  istrl  16540  clwwlkn2  16576  eupthsg  16600  iseupth  16602  eupth2lem1  16613  depind  16664  bj-sseq  16734  bj-charfunbi  16751  bj-nalset  16835  bj-indeq  16869  bj-2inf  16878  strcoll2  16923  strcollnft  16924  strcollnfALT  16926  sscoll2  16928  subctctexmid  16944  domomsubct  16945  exmidsbthrlem  16972  sbthom  16976  qdencn  16977  qdiff  17003  ltlenmkv  17025