Theorem anbi12d 456

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.38  569  pm5.17dc  843  orbididc  894  3anbi123d  1243  xorbi2d  1311  xorbi1d  1312  drsb1  1720  mopick  2019  clelab  2203  cbvrexf  2572  cbvreu  2575  cbvrexdva2  2582  cbvrab  2599  gencbvex  2645  rspce  2696  eqvincf  2720  ceqsrexv  2725  elrabf  2747  rexab2  2758  reu2  2780  reu6  2781  rmo4  2785  reu8  2788  reuind  2795  sbcan  2856  sbcang  2857  sbcabel  2895  rmob  2906  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  difjust  2974  injust  2978  eldif  2982  ssconb  3105  elin  3155  opeq1  3570  opeq2  3571  2ralunsn  3590  elunii  3606  csbunig  3609  eluniab  3613  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab2v  3855  cbvmpt  3872  trel  3882  nalset  3908  elssabg  3923  mss  3981  exss  3982  opelopab2a  4020  poeq1  4054  pocl  4058  soeq1  4070  weeq1  4111  weeq2  4112  ordeq  4127  zfun  4189  snnex  4199  reusv3  4210  ontr2exmid  4268  regexmid  4278  onintexmid  4315  reg3exmid  4322  peano5  4339  limom  4354  nnregexmid  4360  vtoclr  4406  opeliunxp  4413  poinxp  4427  opbrop  4437  csbxpg  4439  opeliunxp2  4494  relop  4504  brcogw  4522  elrnmpt1  4603  elsnres  4665  dfres2  4678  inimasn  4761  xpcanm  4780  xpcan2m  4781  elxp4  4828  elxp5  4829  cnvsom  4881  sbcfung  4945  funopg  4954  fununi  4987  funcnvuni  4988  fneq1  5007  2elresin  5030  feq1  5050  sbcfng  5064  sbcfg  5065  f1eq1  5107  foeq1  5122  f1oeq1  5137  f1oeq2  5138  f1oeq3  5139  ffoss  5178  brprcneu  5191  fv3  5218  tz6.12f  5223  ssimaex  5255  fvopab3g  5266  fvopab3ig  5267  fvopab6  5285  fmptco  5351  elunirn  5426  f1imaeq  5435  foeqcnvco  5450  fliftfun  5456  fliftval  5460  isoeq1  5461  isoeq4  5464  isoini  5477  isopolem  5481  f1oiso2  5486  riotabidv  5490  cbvriota  5498  acexmid  5531  cbvoprab1  5596  cbvoprab2  5597  cbvoprab12  5598  cbvmpt2x  5602  ov  5640  ovig  5642  ovg  5659  caovimo  5714  caoftrn  5756  opabex3d  5768  opabex3  5769  elxp6  5816  unielxp  5820  dfoprab4  5838  dfoprab4f  5839  fmpt2x  5846  xporderlem  5872  poxp  5873  cnvoprab  5875  f1od2  5876  sprmpt2  5880  isprmpt2  5881  dftpos4  5901  tpostpos  5902  smoiso  5940  tfrlem3ag  5947  tfrlem3a  5948  tfr0  5960  tfrlemisucaccv  5962  tfrlemiex  5968  tfrlemi1  5969  tfrlemi14d  5970  tfrexlem  5971  frec0g  6006  frecsuclem3  6013  frecsuc  6014  nnacan  6108  nnmcan  6115  nnaordex  6123  ertr  6144  brecop  6219  eroveu  6220  ecopovtrn  6226  ecopovtrng  6229  th3qlem1  6231  th3qlem2  6232  th3q  6234  xpsnen  6318  endisj  6321  phplem3g  6342  ssfiexmid  6361  domfiexmid  6363  findcard2s  6374  ac6sfi  6379  f1dmvrnfibi  6393  supeq1  6399  supeq3  6403  supeq123d  6404  supmoti  6406  eqsupti  6409  supsnti  6418  isotilem  6419  isoti  6420  supisolem  6421  supisoex  6422  cnvinfex  6431  cnvti  6432  eqinfti  6433  infvalti  6435  ltsopi  6510  recexnq  6580  recmulnqg  6581  ltsonq  6588  lt2addnq  6594  lt2mulnq  6595  ltbtwnnqq  6605  prarloclemarch2  6609  enq0sym  6622  enq0ref  6623  enq0tr  6624  enq0breq  6626  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  nqnq0a  6644  nqnq0m  6645  elinp  6664  prcdnql  6674  prcunqu  6675  prltlu  6677  prdisj  6682  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  ltdfpr  6696  genprndl  6711  genprndu  6712  genpdisj  6713  appdivnq  6753  ltpopr  6785  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  ltexpri  6803  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexpr  6828  aptiprleml  6829  archpr  6833  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  cauappcvgpr  6852  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemcl  6866  caucvgpr  6872  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemopu  6889  caucvgprpr  6902  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  lttrsr  6939  recexgt0sr  6950  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  caucvgsr  6978  ltresr  7007  pitonn  7016  peano1nnnn  7020  peano2nnnn  7021  axprecex  7046  axcnre  7047  axpre-lttrn  7050  peano5nnnn  7058  axcaucvglemcau  7064  axcaucvglemres  7065  axlttrn  7181  letri3  7192  letr  7194  le2add  7548  lt2add  7549  ltleadd  7550  lt2sub  7564  le2sub  7565  apreap  7687  apreim  7703  apti  7722  msq11  7980  dfinfre  8034  cju  8038  peano5nni  8042  1nn  8050  peano2nn  8051  nn2ge  8071  nominpos  8268  elz2  8419  dfuzi  8457  uzind  8458  supinfneg  8683  infsupneg  8684  xrletri3  8875  xrletr  8878  z2ge  8893  elixx1  8920  elioo2  8944  iooshf  8975  iooneg  9010  iccneg  9011  icoshft  9012  elfz1  9034  fzdifsuc  9098  fzrev  9101  1fv  9149  qbtwnzlemstep  9257  qbtwnzlemshrink  9258  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2zlemshrink  9262  rebtwn2z  9263  qbtwnre  9265  qbtwnxr  9266  flval  9276  flqlelt  9278  flqbi  9292  flqbi2  9293  modqid2  9353  q2submod  9387  nnesq  9592  shftlem  9704  shftfibg  9708  shftfib  9711  shftfn  9712  2shfti  9719  cjval  9732  cjth  9733  remim  9747  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  rexanuz2  9877  recvguniq  9881  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  rsqrmo  9913  resqrtcl  9915  rersqrtthlem  9916  absdiflt  9978  absdifle  9979  cau3lem  10000  icodiamlt  10066  maxleast  10099  negfi  10110  minmax  10112  lemininf  10115  ltmininf  10116  clim  10120  clim2  10122  climshftlemg  10141  addcn2  10149  climcau  10184  sumeq1  10192  divalgmod  10327  ndvdssub  10330  zsupcllemstep  10341  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  gcddvds  10355  dvdslegcd  10356  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  gcddiv  10408  lcmval  10445  lcmcllem  10449  dvdslcm  10451  lcmledvds  10452  lcmgcdlem  10459  lcmdvds  10461  coprmgcdb  10470  ncoprmgcdne1b  10471  coprmdvds1  10473  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  isprm3  10500  pw2dvdslemn  10543  pw2dvdseu  10546  oddpwdclemxy  10547  bj-sseq  10602  bj-nalset  10686  bj-indeq  10724  bj-2inf  10733  qdencn  10785