Theorem anbi12i 460

Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12.1	⊢ (𝜑 ↔ 𝜓)
anbi12.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
anbi12i	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi1i 458	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 457	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ∧ 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:  anbi12ci  461  ordir  818  orddi  821  3anbi123i  1190  an6  1332  xorcom  1399  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  nford  1581  nfand  1582  sbequ8  1861  sbanv  1904  sban  1974  sbbi  1978  sbnf2  2000  eu1  2070  2exeu  2137  2eu4  2138  sbabel  2366  neanior  2454  rexeqbii  2510  r19.26m  2628  reean  2666  reu5  2714  reu2  2952  reu3  2954  eqss  3199  unss  3338  ralunb  3345  ssin  3386  undi  3412  difundi  3416  indifdir  3420  inab  3432  difab  3433  reuss2  3444  reupick  3448  raaan  3557  prss  3779  tpss  3789  prsspw  3796  prneimg  3805  uniin  3860  intun  3906  intpr  3907  disjiun  4029  brin  4086  brdif  4087  ssext  4255  pweqb  4257  opthg2  4273  copsex4g  4281  opelopabsb  4295  eqopab2b  4315  pwin  4318  pofun  4348  wetrep  4396  ordwe  4613  wessep  4615  reg3exmidlemwe  4616  elxp3  4718  soinxp  4734  relun  4781  inopab  4799  difopab  4800  inxp  4801  opelco2g  4835  cnvco  4852  dmin  4875  restidsing  5003  intasym  5055  asymref  5056  cnvdif  5077  xpm  5092  xp11m  5109  dfco2  5170  relssdmrn  5191  cnvpom  5213  xpcom  5217  dffun4  5270  dffun4f  5275  funun  5303  funcnveq  5322  fun11  5326  fununi  5327  imadif  5339  imainlem  5340  imain  5341  fnres  5377  fnopabg  5384  fun  5433  fin  5447  dff1o2  5512  brprcneu  5554  fsn  5737  dff1o6  5826  isotr  5866  brabvv  5972  eqoprab2b  5984  fvmpopr2d  6063  dfoprab3  6258  poxp  6299  cnvoprab  6301  f1od2  6302  brtpos2  6318  tfrlem7  6384  dfer2  6602  eqer  6633  iinerm  6675  brecop  6693  eroveu  6694  erovlem  6695  oviec  6709  mapval2  6746  ixpin  6791  xpcomco  6894  xpassen  6898  ssenen  6921  sbthlemi10  7041  infmoti  7103  dfmq0qs  7515  dfplq0qs  7516  enq0enq  7517  enq0tr  7520  npsspw  7557  nqprdisj  7630  ltnqpr  7679  ltnqpri  7680  ltexprlemdisj  7692  addcanprg  7702  recexprlemdisj  7716  caucvgprprlemval  7774  addsrpr  7831  mulsrpr  7832  mulgt0sr  7864  addcnsr  7920  mulcnsr  7921  ltresr  7925  addvalex  7930  axcnre  7967  axpre-suploc  7988  supinfneg  9688  infsupneg  9689  xrnemnf  9871  xrnepnf  9872  elfzuzb  10113  fzass4  10156  infssuzex  10342  hashfacen  10947  rexanre  11404  cbvprod  11742  nnwosdc  12233  isprm3  12313  issubm  13176  issubmd  13178  0subm  13188  insubm  13189  isnsg2  13411  lss1d  14017  tgval2  14395  epttop  14434  cnnei  14576  txuni2  14600  txbas  14602  txdis1cn  14622  xmeterval  14779  dedekindicc  14977  plyun0  15080  lgslem3  15351  bj-stan  15501  nnti  15747