Theorem anbi12d 465

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 461	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 460	. 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  595  pm5.17dc  890  orbididc  938  3anbi123d  1291  xorbi2d  1359  xorbi1d  1360  drsb1  1772  mopick  2078  clelab  2266  cbvrexf  2652  cbvreu  2655  cbvrexdva2  2665  cbvrab  2687  gencbvex  2735  rspce  2788  eqvincf  2814  ceqsrexv  2819  elrabf  2842  rexab2  2854  reu2  2876  reu6  2877  rmo4  2881  reu8  2884  reuind  2893  sbcan  2955  sbcang  2956  sbcabel  2994  rmob  3005  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  difjust  3077  injust  3081  eldif  3085  ssconb  3214  elin  3264  opeq1  3713  opeq2  3714  2ralunsn  3733  elunii  3749  csbunig  3752  eluniab  3756  cbvopab  4007  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  cbvopab2v  4013  cbvmptf  4030  cbvmpt  4031  trel  4041  nalset  4066  elssabg  4081  mss  4156  exss  4157  opelopab2a  4195  poeq1  4229  pocl  4233  soeq1  4245  weeq1  4286  weeq2  4287  ordeq  4302  zfun  4364  snnex  4377  reusv3  4389  ontr2exmid  4448  regexmid  4458  onintexmid  4495  reg3exmid  4502  peano5  4520  limom  4535  nnregexmid  4542  vtoclr  4595  opeliunxp  4602  poinxp  4616  opbrop  4626  csbxpg  4628  opeliunxp2  4687  relop  4697  brcogw  4716  elrnmpt1  4798  elsnres  4864  dfres2  4879  inimasn  4964  xpcanm  4986  xpcan2m  4987  elxp4  5034  elxp5  5035  cnvsom  5090  sbcfung  5155  funopg  5165  fununi  5199  funcnvuni  5200  fneq1  5219  2elresin  5242  feq1  5263  sbcfng  5278  sbcfg  5279  f1eq1  5331  foeq1  5349  f1oeq1  5364  f1oeq2  5365  f1oeq3  5366  ffoss  5407  brprcneu  5422  fv3  5452  tz6.12f  5458  ssimaex  5490  fvopab3g  5502  fvopab3ig  5503  fvopab6  5525  fmptco  5594  elunirn  5675  f1imaeq  5684  foeqcnvco  5699  fliftfun  5705  fliftval  5709  isoeq1  5710  isoeq4  5713  isoini  5727  isopolem  5731  f1oiso2  5736  riotabidv  5740  cbvriota  5748  acexmid  5781  ovanraleqv  5806  cbvoprab1  5851  cbvoprab2  5852  cbvoprab12  5853  cbvmpox  5857  ov  5898  ovig  5900  ovg  5917  caovimo  5972  caoftrn  6015  opabex3d  6027  opabex3  6028  elxp6  6075  unielxp  6080  dfoprab4  6098  dfoprab4f  6099  fmpox  6106  xporderlem  6136  poxp  6137  cnvoprab  6139  f1od2  6140  opeliunxp2f  6143  rbropapd  6147  dftpos4  6168  tpostpos  6169  smoiso  6207  tfrlem3ag  6214  tfrlem3a  6215  tfr0dm  6227  tfrlemisucaccv  6230  tfrlemiex  6236  tfrlemi1  6237  tfrlemi14d  6238  tfrexlem  6239  tfr1onlem3ag  6242  tfr1onlemsucaccv  6246  tfr1onlemex  6252  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemex  6265  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  frec0g  6302  frecabcl  6304  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  nnacan  6416  nnmcan  6423  nnaordex  6431  ertr  6452  brecop  6527  eroveu  6528  ecopovtrn  6534  ecopovtrng  6537  th3qlem1  6539  th3qlem2  6540  th3q  6542  elpm2r  6568  mapsncnv  6597  elixp2  6604  ixpeq1  6611  elixpsn  6637  ixpsnf1o  6638  mapsnen  6713  map1  6714  xpsnen  6723  endisj  6726  xpf1o  6746  phplem3g  6758  ssfiexmid  6778  domfiexmid  6780  findcard2s  6792  isinfinf  6799  ac6sfi  6800  fiintim  6825  fisseneq  6828  f1dmvrnfibi  6840  sbthlem2  6854  isbth  6863  supeq1  6881  supeq3  6885  supeq123d  6886  supmoti  6888  eqsupti  6891  supsnti  6900  isotilem  6901  isoti  6902  supisolem  6903  supisoex  6904  cnvinfex  6913  cnvti  6914  eqinfti  6915  infvalti  6917  updjud  6975  ctssexmid  7032  omniwomnimkv  7049  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  cc2lem  7098  cc3  7100  ltsopi  7152  recexnq  7222  recmulnqg  7223  ltsonq  7230  lt2addnq  7236  lt2mulnq  7237  ltbtwnnqq  7247  prarloclemarch2  7251  enq0sym  7264  enq0ref  7265  enq0tr  7266  enq0breq  7268  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  nqnq0a  7286  nqnq0m  7287  elinp  7306  prcdnql  7316  prcunqu  7317  prltlu  7319  prdisj  7324  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  ltdfpr  7338  genprndl  7353  genprndu  7354  genpdisj  7355  appdivnq  7395  ltpopr  7427  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  ltexpri  7445  recexprlemm  7456  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  recexpr  7470  aptiprleml  7471  archpr  7475  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemcl  7508  caucvgpr  7514  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemopu  7531  caucvgprpr  7544  suplocexpr  7557  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  lttrsr  7594  recexgt0sr  7605  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  caucvgsr  7634  suplocsrlem  7640  ltresr  7671  pitonn  7680  peano1nnnn  7684  peano2nnnn  7685  axprecex  7712  axcnre  7713  axpre-lttrn  7716  peano5nnnn  7724  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  axlttrn  7857  axsuploc  7861  letri3  7869  letr  7871  le2add  8230  lt2add  8231  ltleadd  8232  lt2sub  8246  le2sub  8247  apreap  8373  apreim  8389  apti  8408  msq11  8684  dfinfre  8738  sup3exmid  8739  cju  8743  peano5nni  8747  1nn  8755  peano2nn  8756  nn2ge  8777  nominpos  8981  elz2  9146  dfuzi  9185  uzind  9186  supinfneg  9417  infsupneg  9418  elpqb  9468  xrletri3  9618  xrletr  9621  z2ge  9639  elixx1  9710  elioo2  9734  iooshf  9765  iooneg  9801  iccneg  9802  icoshft  9803  elfz1  9826  fzdifsuc  9892  fzrev  9895  1fv  9947  exbtwnzlemstep  10056  exbtwnzlemshrink  10057  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2zlemshrink  10062  rebtwn2z  10063  qbtwnre  10065  qbtwnxr  10066  flval  10076  flqlelt  10080  flqbi  10094  flqbi2  10095  modqid2  10155  q2submod  10189  nnesq  10442  hashunlem  10582  zfz1isolem1  10615  zfz1iso  10616  seq3coll  10617  shftlem  10620  shftfibg  10624  shftfib  10627  shftfn  10628  2shfti  10635  cjval  10649  cjth  10650  remim  10664  caucvgrelemcau  10784  caucvgre  10785  cvg1nlemcau  10788  cvg1nlemres  10789  rexanuz2  10795  recvguniq  10799  resqrexlemgt0  10824  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  rsqrmo  10831  resqrtcl  10833  rersqrtthlem  10834  absdiflt  10896  absdifle  10897  cau3lem  10918  icodiamlt  10984  maxleast  11017  negfi  11031  minmax  11033  lemininf  11037  ltmininf  11038  xrmaxlesup  11060  xrminmax  11066  xrltmininf  11071  xrlemininf  11072  iooinsup  11078  clim  11082  clim2  11084  climshftlemg  11103  addcn2  11111  climcau  11148  summodc  11184  fsum3  11188  fsum2dlemstep  11235  fisumcom2  11239  fsum00  11263  ntrivcvgap0  11350  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  prodmodc  11379  zproddc  11380  fprodseq  11384  sin01bnd  11500  cos01bnd  11501  divalgmod  11660  ndvdssub  11663  zsupcllemstep  11674  infssuzex  11678  gcdsupex  11682  gcdsupcl  11683  gcddvds  11688  dvdslegcd  11689  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemeu  11731  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dfgcd2  11738  gcddiv  11743  lcmval  11780  lcmcllem  11784  dvdslcm  11786  lcmledvds  11787  lcmgcdlem  11794  lcmdvds  11796  coprmgcdb  11805  ncoprmgcdne1b  11806  coprmdvds1  11808  qredeu  11814  divgcdcoprm0  11818  divgcdcoprmex  11819  isprm3  11835  pw2dvdslemn  11879  pw2dvdseu  11882  oddpwdclemxy  11883  qnumdencl  11901  qnumdenbi  11906  crth  11936  ennnfonelemim  11973  exmidunben  11975  ctinfom  11977  ctiunctlemu1st  11983  ctiunctlemu2nd  11984  ctiunctlemudc  11986  ctiunctlemfo  11988  istopg  12205  fiinbas  12255  eltg2  12261  topbas  12275  neiint  12353  neipsm  12362  opnneissb  12363  opnssneib  12364  innei  12371  restbasg  12376  iscnp4  12426  cnpnei  12427  cnconst2  12441  cnptopresti  12446  cnptoprest  12447  cnpdis  12450  lmss  12454  lmres  12456  txbas  12466  eltx  12467  neitx  12476  txcnp  12479  txcnmpt  12481  uptx  12482  txdis  12485  txdis1cn  12486  txlm  12487  txhmeo  12527  ispsmet  12531  ismet  12552  isxmet  12553  bldisj  12609  blininf  12632  blssexps  12637  blssex  12638  ssblex  12639  xmspropd  12685  mspropd  12686  neibl  12699  metequiv  12703  bdmopn  12712  metrest  12714  xmetxp  12715  xmetxpbl  12716  xmettx  12718  metcnp3  12719  tgioo  12754  tgqioo  12755  addcncntoplem  12759  mulcncflem  12798  dedekindeu  12809  dedekindicclemicc  12818  limccl  12836  ellimc3apf  12837  limcimolemlt  12841  limccoap  12855  sin0pilem2  12911  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  bj-sseq  13170  bj-nalset  13264  bj-indeq  13298  bj-2inf  13307  strcoll2  13352  strcollnft  13353  strcollnfALT  13355  sscoll2  13357  subctctexmid  13369  exmidsbthrlem  13392  sbthom  13396  qdencn  13397