Theorem anbi12d 464

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 460	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 459	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.38  594  pm5.17dc  889  orbididc  937  3anbi123d  1290  xorbi2d  1358  xorbi1d  1359  drsb1  1771  mopick  2075  clelab  2263  cbvrexf  2647  cbvreu  2650  cbvrexdva2  2657  cbvrab  2679  gencbvex  2727  rspce  2779  eqvincf  2805  ceqsrexv  2810  elrabf  2833  rexab2  2845  reu2  2867  reu6  2868  rmo4  2872  reu8  2875  reuind  2884  sbcan  2946  sbcang  2947  sbcabel  2985  rmob  2996  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  difjust  3067  injust  3071  eldif  3075  ssconb  3204  elin  3254  opeq1  3700  opeq2  3701  2ralunsn  3720  elunii  3736  csbunig  3739  eluniab  3743  cbvopab  3994  cbvopab1  3996  cbvopab2  3997  cbvopab1s  3998  cbvopab2v  4000  cbvmptf  4017  cbvmpt  4018  trel  4028  nalset  4053  elssabg  4068  mss  4143  exss  4144  opelopab2a  4182  poeq1  4216  pocl  4220  soeq1  4232  weeq1  4273  weeq2  4274  ordeq  4289  zfun  4351  snnex  4364  reusv3  4376  ontr2exmid  4435  regexmid  4445  onintexmid  4482  reg3exmid  4489  peano5  4507  limom  4522  nnregexmid  4529  vtoclr  4582  opeliunxp  4589  poinxp  4603  opbrop  4613  csbxpg  4615  opeliunxp2  4674  relop  4684  brcogw  4703  elrnmpt1  4785  elsnres  4851  dfres2  4866  inimasn  4951  xpcanm  4973  xpcan2m  4974  elxp4  5021  elxp5  5022  cnvsom  5077  sbcfung  5142  funopg  5152  fununi  5186  funcnvuni  5187  fneq1  5206  2elresin  5229  feq1  5250  sbcfng  5265  sbcfg  5266  f1eq1  5318  foeq1  5336  f1oeq1  5351  f1oeq2  5352  f1oeq3  5353  ffoss  5392  brprcneu  5407  fv3  5437  tz6.12f  5443  ssimaex  5475  fvopab3g  5487  fvopab3ig  5488  fvopab6  5510  fmptco  5579  elunirn  5660  f1imaeq  5669  foeqcnvco  5684  fliftfun  5690  fliftval  5694  isoeq1  5695  isoeq4  5698  isoini  5712  isopolem  5716  f1oiso2  5721  riotabidv  5725  cbvriota  5733  acexmid  5766  ovanraleqv  5791  cbvoprab1  5836  cbvoprab2  5837  cbvoprab12  5838  cbvmpox  5842  ov  5883  ovig  5885  ovg  5902  caovimo  5957  caoftrn  6000  opabex3d  6012  opabex3  6013  elxp6  6060  unielxp  6065  dfoprab4  6083  dfoprab4f  6084  fmpox  6091  xporderlem  6121  poxp  6122  cnvoprab  6124  f1od2  6125  opeliunxp2f  6128  rbropapd  6132  dftpos4  6153  tpostpos  6154  smoiso  6192  tfrlem3ag  6199  tfrlem3a  6200  tfr0dm  6212  tfrlemisucaccv  6215  tfrlemiex  6221  tfrlemi1  6222  tfrlemi14d  6223  tfrexlem  6224  tfr1onlem3ag  6227  tfr1onlemsucaccv  6231  tfr1onlemex  6237  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllemex  6250  tfrcllemaccex  6251  tfrcllemres  6252  tfrcldm  6253  frec0g  6287  frecabcl  6289  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecsuc  6297  nnacan  6401  nnmcan  6408  nnaordex  6416  ertr  6437  brecop  6512  eroveu  6513  ecopovtrn  6519  ecopovtrng  6522  th3qlem1  6524  th3qlem2  6525  th3q  6527  elpm2r  6553  mapsncnv  6582  elixp2  6589  ixpeq1  6596  elixpsn  6622  ixpsnf1o  6623  mapsnen  6698  map1  6699  xpsnen  6708  endisj  6711  xpf1o  6731  phplem3g  6743  ssfiexmid  6763  domfiexmid  6765  findcard2s  6777  isinfinf  6784  ac6sfi  6785  fiintim  6810  fisseneq  6813  f1dmvrnfibi  6825  sbthlem2  6839  isbth  6848  supeq1  6866  supeq3  6870  supeq123d  6871  supmoti  6873  eqsupti  6876  supsnti  6885  isotilem  6886  isoti  6887  supisolem  6888  supisoex  6889  cnvinfex  6898  cnvti  6899  eqinfti  6900  infvalti  6902  updjud  6960  ctssexmid  7017  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  acfun  7056  ccfunen  7072  ltsopi  7121  recexnq  7191  recmulnqg  7192  ltsonq  7199  lt2addnq  7205  lt2mulnq  7206  ltbtwnnqq  7216  prarloclemarch2  7220  enq0sym  7233  enq0ref  7234  enq0tr  7235  enq0breq  7237  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  mulnnnq0  7251  nqnq0a  7255  nqnq0m  7256  elinp  7275  prcdnql  7285  prcunqu  7286  prltlu  7288  prdisj  7293  prarloclemlo  7295  prarloclem3  7298  prarloclem5  7301  ltdfpr  7307  genprndl  7322  genprndu  7323  genpdisj  7324  appdivnq  7364  ltpopr  7396  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  ltexpri  7414  recexprlemm  7425  recexprlemdisj  7431  recexprlemloc  7432  recexprlem1ssl  7434  recexprlem1ssu  7435  recexpr  7439  aptiprleml  7440  archpr  7444  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlemlim  7462  cauappcvgpr  7463  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemcl  7477  caucvgpr  7483  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemopu  7500  caucvgprpr  7513  suplocexpr  7526  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  lttrsr  7563  recexgt0sr  7574  caucvgsrlemcau  7594  caucvgsrlemgt1  7596  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  caucvgsr  7603  suplocsrlem  7609  ltresr  7640  pitonn  7649  peano1nnnn  7653  peano2nnnn  7654  axprecex  7681  axcnre  7682  axpre-lttrn  7685  peano5nnnn  7693  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  axlttrn  7826  axsuploc  7830  letri3  7838  letr  7840  le2add  8199  lt2add  8200  ltleadd  8201  lt2sub  8215  le2sub  8216  apreap  8342  apreim  8358  apti  8377  msq11  8653  dfinfre  8707  sup3exmid  8708  cju  8712  peano5nni  8716  1nn  8724  peano2nn  8725  nn2ge  8746  nominpos  8950  elz2  9115  dfuzi  9154  uzind  9155  supinfneg  9383  infsupneg  9384  xrletri3  9581  xrletr  9584  z2ge  9602  elixx1  9673  elioo2  9697  iooshf  9728  iooneg  9764  iccneg  9765  icoshft  9766  elfz1  9788  fzdifsuc  9854  fzrev  9857  1fv  9909  exbtwnzlemstep  10018  exbtwnzlemshrink  10019  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2zlemshrink  10024  rebtwn2z  10025  qbtwnre  10027  qbtwnxr  10028  flval  10038  flqlelt  10042  flqbi  10056  flqbi2  10057  modqid2  10117  q2submod  10151  nnesq  10404  hashunlem  10543  zfz1isolem1  10576  zfz1iso  10577  seq3coll  10578  shftlem  10581  shftfibg  10585  shftfib  10588  shftfn  10589  2shfti  10596  cjval  10610  cjth  10611  remim  10625  caucvgrelemcau  10745  caucvgre  10746  cvg1nlemcau  10749  cvg1nlemres  10750  rexanuz2  10756  recvguniq  10760  resqrexlemgt0  10785  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemsqa  10789  resqrexlemex  10790  rsqrmo  10792  resqrtcl  10794  rersqrtthlem  10795  absdiflt  10857  absdifle  10858  cau3lem  10879  icodiamlt  10945  maxleast  10978  negfi  10992  minmax  10994  lemininf  10998  ltmininf  10999  xrmaxlesup  11021  xrminmax  11027  xrltmininf  11032  xrlemininf  11033  iooinsup  11039  clim  11043  clim2  11045  climshftlemg  11064  addcn2  11072  climcau  11109  summodc  11145  fsum3  11149  fsum2dlemstep  11196  fisumcom2  11200  fsum00  11224  ntrivcvgap0  11311  prodeq1f  11314  prodeq2w  11318  prodeq2  11319  sin01bnd  11453  cos01bnd  11454  divalgmod  11613  ndvdssub  11616  zsupcllemstep  11627  infssuzex  11631  gcdsupex  11635  gcdsupcl  11636  gcddvds  11641  dvdslegcd  11642  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemzz  11679  bezoutlemeu  11684  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dfgcd2  11691  gcddiv  11696  lcmval  11733  lcmcllem  11737  dvdslcm  11739  lcmledvds  11740  lcmgcdlem  11747  lcmdvds  11749  coprmgcdb  11758  ncoprmgcdne1b  11759  coprmdvds1  11761  qredeu  11767  divgcdcoprm0  11771  divgcdcoprmex  11772  isprm3  11788  pw2dvdslemn  11832  pw2dvdseu  11835  oddpwdclemxy  11836  qnumdencl  11854  qnumdenbi  11859  crth  11889  ennnfonelemim  11926  exmidunben  11928  ctinfom  11930  ctiunctlemu1st  11936  ctiunctlemu2nd  11937  ctiunctlemudc  11939  ctiunctlemfo  11941  istopg  12155  fiinbas  12205  eltg2  12211  topbas  12225  neiint  12303  neipsm  12312  opnneissb  12313  opnssneib  12314  innei  12321  restbasg  12326  iscnp4  12376  cnpnei  12377  cnconst2  12391  cnptopresti  12396  cnptoprest  12397  cnpdis  12400  lmss  12404  lmres  12406  txbas  12416  eltx  12417  neitx  12426  txcnp  12429  txcnmpt  12431  uptx  12432  txdis  12435  txdis1cn  12436  txlm  12437  txhmeo  12477  ispsmet  12481  ismet  12502  isxmet  12503  bldisj  12559  blininf  12582  blssexps  12587  blssex  12588  ssblex  12589  xmspropd  12635  mspropd  12636  neibl  12649  metequiv  12653  bdmopn  12662  metrest  12664  xmetxp  12665  xmetxpbl  12666  xmettx  12668  metcnp3  12669  tgioo  12704  tgqioo  12705  addcncntoplem  12709  mulcncflem  12748  dedekindeu  12759  dedekindicclemicc  12768  limccl  12786  ellimc3apf  12787  limcimolemlt  12791  limccoap  12805  sin0pilem2  12852  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  bj-sseq  12988  bj-nalset  13082  bj-indeq  13116  bj-2inf  13125  subctctexmid  13185  exmidsbthrlem  13206  sbthom  13210  qdencn  13211