Theorem anbi12i 464

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 462	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 461	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi12ci  465  ordir  829  orddi  832  3anbi123i  1219  an6  1362  xorcom  1437  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  nford  1620  nfand  1621  sbequ8  1900  sbanv  1944  sban  2015  sbbi  2019  sbnf2  2041  eu1  2111  2exeu  2179  2eu4  2180  sbabel  2419  neanior  2507  rexeqbii  2563  r19.26m  2682  reean  2720  reu5  2770  cbvreuw  2781  reu2  3014  reu3  3016  eqss  3263  unss  3403  ralunb  3410  ssin  3453  undi  3479  difundi  3483  indifdir  3487  inab  3499  difab  3500  reuss2  3513  reupick  3517  raaan  3633  prss  3871  tpss  3883  prsspw  3890  prneimg  3899  uniin  3955  intun  4001  intpr  4002  disjiun  4125  brin  4183  brdif  4184  ssext  4361  pweqb  4363  opthg2  4379  copsex4g  4387  opelopabsb  4402  eqopab2b  4422  pwin  4427  pofun  4457  wetrep  4505  ordwe  4723  wessep  4725  reg3exmidlemwe  4726  elxp3  4829  soinxp  4845  relun  4894  inopab  4912  difopab  4913  inxp  4914  opelco2g  4948  cnvco  4965  dmin  4989  restidsing  5119  intasym  5172  asymref  5173  cnvdif  5194  xpm  5209  xp11m  5226  dfco2  5287  relssdmrn  5308  cnvpom  5330  xpcom  5334  dffun4  5388  dffun4f  5393  funun  5422  funcnveq  5444  fun11  5448  fununi  5449  imadif  5461  imainlem  5462  imain  5463  fnres  5500  fnopabg  5507  fun  5561  fin  5578  dff1o2  5644  brprcneu  5688  fsn  5880  dff1o6  5982  isotr  6022  brabvv  6134  eqoprab2b  6146  fvmpopr2d  6225  dfoprab3  6425  poxp  6468  cnvoprab  6470  f1od2  6471  brtpos2  6522  tfrlem7  6588  dfer2  6808  eqer  6839  iinerm  6881  brecop  6899  eroveu  6900  erovlem  6901  oviec  6915  mapval2  6959  ixpin  7005  modom  7108  xpcomco  7124  xpassen  7128  ssenen  7152  sbthlemi10  7283  infmoti  7368  dfmq0qs  7796  dfplq0qs  7797  enq0enq  7798  enq0tr  7801  npsspw  7838  nqprdisj  7911  ltnqpr  7960  ltnqpri  7961  ltexprlemdisj  7973  addcanprg  7983  recexprlemdisj  7997  caucvgprprlemval  8055  addsrpr  8112  mulsrpr  8113  mulgt0sr  8145  addcnsr  8201  mulcnsr  8202  ltresr  8206  addvalex  8211  axcnre  8248  axpre-suploc  8269  supinfneg  9995  infsupneg  9996  xrnemnf  10179  xrnepnf  10180  elfzuzb  10422  fzass4  10468  infssuzex  10666  hashfibclem  11282  hashfacen  11284  rexanre  11986  cbvprod  12325  nnwosdc  12816  isprm3  12896  issubm  13779  issubmd  13781  0subm  13791  insubm  13792  isnsg2  14006  lss1d  14720  tgval2  15152  epttop  15191  cnnei  15333  txuni2  15357  txbas  15359  txdis1cn  15379  xmeterval  15536  dedekindicc  15734  plyun0  15837  lgslem3  16121  vtxd0nedgbfi  16540  wlk1walkdom  16600  clwwlknonccat  16674  clwwlknon2x  16676  bj-stan  16775  nnti  17022  dfrals2  17130  alsbii  17141  ralsbii  17142  cbvals  17146  rals-no-surprise  17148  dfralseu2  17164  alseubii  17173  ralseubii  17174