Theorem anbi12d 442

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

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.38  537  pm5.17dc  810  orbididc  860  3anbi123d  1207  xorbi2d  1271  xorbi1d  1272  drsb1  1680  mopick  1978  clelab  2162  cbvrexf  2528  cbvreu  2531  cbvrexdva2  2538  cbvrab  2555  gencbvex  2600  rspce  2651  eqvincf  2669  ceqsrexv  2674  elrabf  2696  rexab2  2707  reu2  2729  reu6  2730  rmo4  2734  reu8  2737  reuind  2744  sbcan  2805  sbcang  2806  sbcabel  2839  rmob  2850  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  difjust  2919  injust  2923  eldif  2927  psseq1  3031  psseq2  3032  ssconb  3076  elin  3126  opeq1  3549  opeq2  3550  2ralunsn  3569  elunii  3585  csbunig  3588  eluniab  3592  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  cbvmpt  3851  trel  3861  nalset  3887  elssabg  3902  mss  3962  exss  3963  opelopab2a  4002  poeq1  4036  pocl  4040  soeq1  4052  weeq1  4093  weeq2  4094  ordeq  4109  zfun  4171  snnex  4181  reusv3  4192  ontr2exmid  4250  regexmid  4260  onintexmid  4297  reg3exmid  4304  peano5  4321  limom  4336  nnregexmid  4342  vtoclr  4388  opeliunxp  4395  poinxp  4409  opbrop  4419  csbxpg  4421  opeliunxp2  4476  relop  4486  brcogw  4504  elrnmpt1  4585  elsnres  4647  dfres2  4658  inimasn  4741  xpcanm  4760  xpcan2m  4761  elxp4  4808  elxp5  4809  cnvsom  4861  sbcfung  4925  funopg  4934  fununi  4967  funcnvuni  4968  fneq1  4987  2elresin  5010  feq1  5030  sbcfng  5044  sbcfg  5045  f1eq1  5087  foeq1  5102  f1oeq1  5117  f1oeq2  5118  f1oeq3  5119  ffoss  5158  brprcneu  5171  fv3  5197  tz6.12f  5202  ssimaex  5234  fvopab3g  5245  fvopab3ig  5246  fvopab6  5264  fmptco  5330  elunirn  5405  f1imaeq  5414  f1imapss  5415  foeqcnvco  5430  fliftfun  5436  fliftval  5440  isoeq1  5441  isoeq4  5444  isoini  5457  isopolem  5461  f1oiso2  5466  riotabidv  5470  cbvriota  5478  acexmid  5511  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvmpt2x  5582  ov  5620  ovig  5622  ovg  5639  caovimo  5694  caoftrn  5736  opabex3d  5748  opabex3  5749  elxp6  5796  unielxp  5800  dfoprab4  5818  dfoprab4f  5819  fmpt2x  5826  xporderlem  5852  poxp  5853  sprmpt2  5857  isprmpt2  5858  dftpos4  5878  tpostpos  5879  smoiso  5917  tfrlem3ag  5924  tfrlem3a  5925  tfr0  5937  tfrlemisucaccv  5939  tfrlemiex  5945  tfrlemi1  5946  tfrlemi14d  5947  tfrexlem  5948  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnacan  6085  nnmcan  6092  nnaordex  6100  ertr  6121  brecop  6196  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  th3qlem2  6209  th3q  6211  xpsnen  6295  endisj  6298  phplem3g  6319  ssfiexmid  6336  findcard2s  6347  ac6sfi  6352  ltsopi  6418  recexnq  6488  recmulnqg  6489  ltsonq  6496  lt2addnq  6502  lt2mulnq  6503  ltbtwnnqq  6513  prarloclemarch2  6517  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  nqnq0a  6552  nqnq0m  6553  elinp  6572  prcdnql  6582  prcunqu  6583  prltlu  6585  prdisj  6590  prarloclemlo  6592  prarloclem3  6595  prarloclem5  6598  ltdfpr  6604  genprndl  6619  genprndu  6620  genpdisj  6621  appdivnq  6661  ltpopr  6693  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  ltexpri  6711  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexpr  6736  aptiprleml  6737  archpr  6741  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemcl  6774  caucvgpr  6780  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemopu  6797  caucvgprpr  6810  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  lttrsr  6847  recexgt0sr  6858  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  caucvgsr  6886  ltresr  6915  pitonn  6924  peano1nnnn  6928  peano2nnnn  6929  axprecex  6954  axcnre  6955  axpre-lttrn  6958  peano5nnnn  6966  axcaucvglemcau  6972  axcaucvglemres  6973  axlttrn  7088  letri3  7099  letr  7101  le2add  7439  lt2add  7440  ltleadd  7441  lt2sub  7455  le2sub  7456  apreap  7578  apreim  7594  apti  7613  msq11  7868  cju  7913  peano5nni  7917  1nn  7925  peano2nn  7926  nn2ge  7946  nominpos  8162  elz2  8312  dfuzi  8348  uzind  8349  xrletri3  8721  xrletr  8724  z2ge  8739  elixx1  8766  elioo2  8790  iooshf  8821  iooneg  8856  iccneg  8857  icoshft  8858  elfz1  8879  fzdifsuc  8943  fzrev  8946  1fv  8996  qbtwnzlemstep  9103  qbtwnzlemshrink  9104  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2zlemshrink  9108  rebtwn2z  9109  qbtwnre  9111  flval  9116  flqlelt  9118  flqbi  9132  flqbi2  9133  nnesq  9368  shftlem  9417  shftfibg  9421  shftfib  9424  shftfn  9425  2shfti  9432  cjval  9445  cjth  9446  remim  9460  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  rexanuz2  9589  recvguniq  9593  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  rsqrmo  9625  resqrtcl  9627  rersqrtthlem  9628  absdiflt  9688  absdifle  9689  cau3lem  9710  icodiamlt  9776  clim  9802  clim2  9804  climshftlemg  9823  addcn2  9831  climcau  9866  sumeq1  9874  bj-sseq  9931  bj-nalset  10015  bj-indeq  10053  bj-2inf  10062  qdencn  10124