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  904  orbididc  953  3anbi123d  1312  xorbi2d  1380  xorbi1d  1381  drsb1  1799  mopick  2104  clelab  2303  cbvrexfw  2695  cbvrexf  2697  cbvreu  2701  cbvrexvw  2708  cbvreuvw  2709  cbvrexdva2  2711  cbvrab  2735  gencbvex  2783  rspce  2836  eqvincf  2862  ceqsrexv  2867  elrabf  2891  rexab2  2903  reu2  2925  reu6  2926  rmo4  2930  reu8  2933  reuind  2942  sbcan  3005  sbcang  3006  sbcabel  3044  rmob  3055  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  difjust  3130  injust  3134  eldif  3138  ssconb  3268  elin  3318  opeq1  3777  opeq2  3778  2ralunsn  3797  elunii  3813  csbunig  3816  eluniab  3820  cbvopab  4072  cbvopab1  4074  cbvopab2  4075  cbvopab1s  4076  cbvopab2v  4078  cbvmptf  4095  cbvmpt  4096  trel  4106  nalset  4131  elssabg  4146  mss  4224  exss  4225  opelopab2a  4263  poeq1  4297  pocl  4301  soeq1  4313  weeq1  4354  weeq2  4355  ordeq  4370  zfun  4432  snnex  4446  reusv3  4458  ontr2exmid  4522  regexmid  4532  onintexmid  4570  reg3exmid  4577  peano5  4595  limom  4611  nnregexmid  4618  vtoclr  4672  opeliunxp  4679  poinxp  4693  opbrop  4703  csbxpg  4705  opeliunxp2  4764  relop  4774  brcogw  4793  elrnmpt1  4875  elsnres  4941  dfres2  4956  inimasn  5043  xpcanm  5065  xpcan2m  5066  elxp4  5113  elxp5  5114  cnvsom  5169  sbcfung  5237  funopg  5247  fununi  5281  funcnvuni  5282  fneq1  5301  2elresin  5324  feq1  5345  sbcfng  5360  sbcfg  5361  f1eq1  5413  foeq1  5431  f1oeq1  5446  f1oeq2  5447  f1oeq3  5448  ffoss  5490  brprcneu  5505  fv3  5535  tz6.12f  5541  ssimaex  5574  fvopab3g  5586  fvopab3ig  5587  fvopab6  5609  fmptco  5679  elunirn  5762  f1imaeq  5771  foeqcnvco  5786  fliftfun  5792  fliftval  5796  isoeq1  5797  isoeq4  5800  isoini  5814  isopolem  5818  f1oiso2  5823  riotabidv  5828  cbvriota  5836  acexmid  5869  ovanraleqv  5894  cbvoprab1  5942  cbvoprab2  5943  cbvoprab12  5944  cbvmpox  5948  ov  5989  ovig  5991  ovg  6008  caovimo  6063  caoftrn  6103  opabex3d  6117  opabex3  6118  elxp6  6165  unielxp  6170  dfoprab4  6188  dfoprab4f  6189  fmpox  6196  xporderlem  6227  poxp  6228  cnvoprab  6230  f1od2  6231  opeliunxp2f  6234  rbropapd  6238  dftpos4  6259  tpostpos  6260  smoiso  6298  tfrlem3ag  6305  tfrlem3a  6306  tfr0dm  6318  tfrlemisucaccv  6321  tfrlemiex  6327  tfrlemi1  6328  tfrlemi14d  6329  tfrexlem  6330  tfr1onlem3ag  6333  tfr1onlemsucaccv  6337  tfr1onlemex  6343  tfr1onlemaccex  6344  tfr1onlemres  6345  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllemex  6356  tfrcllemaccex  6357  tfrcllemres  6358  tfrcldm  6359  frec0g  6393  frecabcl  6395  freccllem  6398  frecfcllem  6400  frecsuclem  6402  frecsuc  6403  nnacan  6508  nnmcan  6515  nnaordex  6524  ertr  6545  brecop  6620  eroveu  6621  ecopovtrn  6627  ecopovtrng  6630  th3qlem1  6632  th3qlem2  6633  th3q  6635  elpm2r  6661  mapsncnv  6690  elixp2  6697  ixpeq1  6704  elixpsn  6730  ixpsnf1o  6731  mapsnen  6806  map1  6807  xpsnen  6816  endisj  6819  xpf1o  6839  phplem3g  6851  ssfiexmid  6871  domfiexmid  6873  findcard2s  6885  isinfinf  6892  ac6sfi  6893  fiintim  6923  fisseneq  6926  f1dmvrnfibi  6938  sbthlem2  6952  isbth  6961  supeq1  6980  supeq3  6984  supeq123d  6985  supmoti  6987  eqsupti  6990  supsnti  6999  isotilem  7000  isoti  7001  supisolem  7002  supisoex  7003  cnvinfex  7012  cnvti  7013  eqinfti  7014  infvalti  7016  updjud  7076  ctssexmid  7143  omniwomnimkv  7160  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  acfun  7201  tapeq1  7246  tapeq2  7247  exmidapne  7254  ccfunen  7258  cc2lem  7260  cc3  7262  ltsopi  7314  recexnq  7384  recmulnqg  7385  ltsonq  7392  lt2addnq  7398  lt2mulnq  7399  ltbtwnnqq  7409  prarloclemarch2  7413  enq0sym  7426  enq0ref  7427  enq0tr  7428  enq0breq  7430  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  mulnnnq0  7444  nqnq0a  7448  nqnq0m  7449  elinp  7468  prcdnql  7478  prcunqu  7479  prltlu  7481  prdisj  7486  prarloclemlo  7488  prarloclem3  7491  prarloclem5  7494  ltdfpr  7500  genprndl  7515  genprndu  7516  genpdisj  7517  appdivnq  7557  ltpopr  7589  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemrl  7604  ltexprlemru  7606  ltexpri  7607  recexprlemm  7618  recexprlemdisj  7624  recexprlemloc  7625  recexprlem1ssl  7627  recexprlem1ssu  7628  recexpr  7632  aptiprleml  7633  archpr  7637  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem1  7653  cauappcvgprlemlim  7655  cauappcvgpr  7656  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemcl  7670  caucvgpr  7676  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemopu  7693  caucvgprpr  7706  suplocexpr  7719  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  lttrsr  7756  recexgt0sr  7767  caucvgsrlemcau  7787  caucvgsrlemgt1  7789  caucvgsrlemoffcau  7792  caucvgsrlemoffres  7794  caucvgsr  7796  suplocsrlem  7802  ltresr  7833  pitonn  7842  peano1nnnn  7846  peano2nnnn  7847  axprecex  7874  axcnre  7875  axpre-lttrn  7878  peano5nnnn  7886  axcaucvglemcau  7892  axcaucvglemres  7893  axpre-suploclemres  7895  axpre-suploc  7896  axlttrn  8020  axsuploc  8024  letri3  8032  letr  8034  le2add  8395  lt2add  8396  ltleadd  8397  lt2sub  8411  le2sub  8412  apreap  8538  apreim  8554  apti  8573  msq11  8853  dfinfre  8907  sup3exmid  8908  cju  8912  peano5nni  8916  1nn  8924  peano2nn  8925  nn2ge  8946  nominpos  9150  elz2  9318  dfuzi  9357  uzind  9358  supinfneg  9589  infsupneg  9590  elpqb  9643  xrletri3  9798  xrletr  9802  z2ge  9820  elixx1  9891  elioo2  9915  iooshf  9946  iooneg  9982  iccneg  9983  icoshft  9984  elfz1  10007  fzdifsuc  10074  fzrev  10077  1fv  10132  exbtwnzlemstep  10241  exbtwnzlemshrink  10242  exbtwnzlemex  10243  exbtwnz  10244  rebtwn2zlemstep  10246  rebtwn2zlemshrink  10247  rebtwn2z  10248  qbtwnre  10250  qbtwnxr  10251  flval  10265  flqlelt  10269  flqbi  10283  flqbi2  10284  modqid2  10344  q2submod  10378  nnesq  10632  hashunlem  10775  zfz1isolem1  10811  zfz1iso  10812  seq3coll  10813  shftlem  10816  shftfibg  10820  shftfib  10823  shftfn  10824  2shfti  10831  cjval  10845  cjth  10846  remim  10860  caucvgrelemcau  10980  caucvgre  10981  cvg1nlemcau  10984  cvg1nlemres  10985  rexanuz2  10991  recvguniq  10995  resqrexlemgt0  11020  resqrexlemoverl  11021  resqrexlemglsq  11022  resqrexlemsqa  11024  resqrexlemex  11025  rsqrmo  11027  resqrtcl  11029  rersqrtthlem  11030  absdiflt  11092  absdifle  11093  cau3lem  11114  icodiamlt  11180  maxleast  11213  negfi  11227  minmax  11229  lemininf  11233  ltmininf  11234  xrmaxlesup  11258  xrminmax  11264  xrltmininf  11269  xrlemininf  11270  iooinsup  11276  clim  11280  clim2  11282  climshftlemg  11301  addcn2  11309  climcau  11346  summodc  11382  fsum3  11386  fsum2dlemstep  11433  fisumcom2  11437  fsum00  11461  ntrivcvgap0  11548  prodeq1f  11551  prodeq2w  11555  prodeq2  11556  prodmodc  11577  zproddc  11578  fprodseq  11582  fprodntrivap  11583  fprod2dlemstep  11621  fprodcom2fi  11625  sin01bnd  11756  cos01bnd  11757  divalgmod  11922  ndvdssub  11925  zsupcllemstep  11936  infssuzex  11940  nninfdcex  11944  zsupssdc  11945  gcdsupex  11948  gcdsupcl  11949  gcddvds  11954  dvdslegcd  11955  bezoutlemmain  11989  bezoutlemex  11992  bezoutlemzz  11993  bezoutlemeu  11998  bezoutlemle  11999  bezoutlemsup  12000  dfgcd3  12001  dfgcd2  12005  gcddiv  12010  lcmval  12053  lcmcllem  12057  dvdslcm  12059  lcmledvds  12060  lcmgcdlem  12067  lcmdvds  12069  coprmgcdb  12078  ncoprmgcdne1b  12079  coprmdvds1  12081  qredeu  12087  divgcdcoprm0  12091  divgcdcoprmex  12092  isprm3  12108  pw2dvdslemn  12155  pw2dvdseu  12158  oddpwdclemxy  12159  qnumdencl  12177  qnumdenbi  12182  crth  12214  reumodprminv  12243  pythagtriplem19  12272  pceu  12285  pczpre  12287  pcdiv  12292  pc11  12320  dvdsprmpweqle  12326  prmpwdvds  12343  pockthi  12346  infpnlem2  12348  elgz  12359  ennnfonelemim  12415  exmidunben  12417  ctinfom  12419  ctiunctlemu1st  12425  ctiunctlemu2nd  12426  ctiunctlemudc  12428  ctiunctlemfo  12430  infpn2  12447  grpidvalg  12722  grpidpropdg  12723  mgmlrid  12728  ismnddef  12749  sgrpidmndm  12751  ismndd  12768  mndpropd  12771  mndinvmod  12774  mnd1  12775  ismhm  12781  mhmpropd  12785  issubm  12791  insubm  12800  grppropd  12821  dfgrp2  12830  isgrpid2  12841  isgrpinv  12854  grplrinv  12855  grpidinv2  12856  grpidinv  12857  dfgrp3mlem  12896  grplactcnv  12900  cmnpropd  12998  ablpropd  12999  dfur2g  13045  issrg  13048  srgideu  13055  srgidmlem  13061  issrgid  13064  srg1zr  13070  isring  13083  ringideu  13100  ringidmlem  13105  isringid  13108  ringid  13109  ringpropd  13117  ring1  13136  oppr0g  13150  oppr1g  13151  reldvdsrsrg  13160  dvdsrvald  13161  dvdsrd  13162  dvdsrtr  13169  unitgrp  13184  dvdsrpropdg  13215  unitpropdg  13216  aprval  13239  aprap  13243  istopg  13279  fiinbas  13329  eltg2  13335  topbas  13349  neiint  13427  neipsm  13436  opnneissb  13437  opnssneib  13438  innei  13445  restbasg  13450  iscnp4  13500  cnpnei  13501  cnconst2  13515  cnptopresti  13520  cnptoprest  13521  cnpdis  13524  lmss  13528  lmres  13530  txbas  13540  eltx  13541  neitx  13550  txcnp  13553  txcnmpt  13555  uptx  13556  txdis  13559  txdis1cn  13560  txlm  13561  txhmeo  13601  ispsmet  13605  ismet  13626  isxmet  13627  bldisj  13683  blininf  13706  blssexps  13711  blssex  13712  ssblex  13713  xmspropd  13759  mspropd  13760  neibl  13773  metequiv  13777  bdmopn  13786  metrest  13788  xmetxp  13789  xmetxpbl  13790  xmettx  13792  metcnp3  13793  tgioo  13828  tgqioo  13829  addcncntoplem  13833  mulcncflem  13872  dedekindeu  13883  dedekindicclemicc  13892  limccl  13910  ellimc3apf  13911  limcimolemlt  13915  limccoap  13929  sin0pilem2  13985  sincosq1sgn  14029  sincosq2sgn  14030  sincosq3sgn  14031  sincosq4sgn  14032  lgsval  14187  lgsdir2lem5  14215  lgsne0  14221  2sqlem8a  14240  2sqlem8  14241  2sqlem9  14242  bj-sseq  14315  bj-charfunbi  14334  bj-nalset  14418  bj-indeq  14452  bj-2inf  14461  strcoll2  14506  strcollnft  14507  strcollnfALT  14509  sscoll2  14511  subctctexmid  14521  exmidsbthrlem  14541  sbthom  14545  qdencn  14546  ltlenmkv  14588