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  10004  infsupneg  10005  xrnemnf  10189  xrnepnf  10190  elfzuzb  10432  fzass4  10478  infssuzex  10676  hashfibclem  11296  hashfacen  11298  rexanre  12001  cbvprod  12341  nnwosdc  12832  isprm3  12912  issubm  13828  issubmd  13830  0subm  13840  insubm  13841  isnsg2  14055  lss1d  14769  tgval2  15201  epttop  15240  cnnei  15382  txuni2  15406  txbas  15408  txdis1cn  15428  xmeterval  15585  dedekindicc  15783  plyun0  15886  lgslem3  16219  vtxd0nedgbfi  16638  wlk1walkdom  16698  clwwlknonccat  16772  clwwlknon2x  16774  bj-stan  16873  nnti  17120  dfrals2  17228  alsbii  17239  ralsbii  17240  cbvals  17244  rals-no-surprise  17246  dfralseu2  17262  alseubii  17271  ralseubii  17272