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  7369  dfmq0qs  7797  dfplq0qs  7798  enq0enq  7799  enq0tr  7802  npsspw  7839  nqprdisj  7912  ltnqpr  7961  ltnqpri  7962  ltexprlemdisj  7974  addcanprg  7984  recexprlemdisj  7998  caucvgprprlemval  8056  addsrpr  8113  mulsrpr  8114  mulgt0sr  8146  addcnsr  8202  mulcnsr  8203  ltresr  8207  addvalex  8212  axcnre  8249  axpre-suploc  8270  supinfneg  10005  infsupneg  10006  xrnemnf  10190  xrnepnf  10191  elfzuzb  10433  fzass4  10479  infssuzex  10677  hashfibclem  11298  hashfacen  11300  rexanre  12003  cbvprod  12344  nnwosdc  12835  isprm3  12915  issubm  13832  issubmd  13834  0subm  13844  insubm  13845  isnsg2  14059  lss1d  14804  tgval2  15243  epttop  15282  cnnei  15424  txuni2  15448  txbas  15450  txdis1cn  15470  xmeterval  15627  dedekindicc  15825  plyun0  15928  lgslem3  16287  vtxd0nedgbfi  16706  wlk1walkdom  16766  clwwlknonccat  16840  clwwlknon2x  16842  bj-stan  16941  nnti  17188  dfrals2  17297  alsbii  17308  ralsbii  17309  cbvals  17313  rals-no-surprise  17315  dfralseu2  17331  alseubii  17340  ralseubii  17341