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 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

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  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  3630  prss  3866  tpss  3878  prsspw  3885  prneimg  3894  uniin  3950  intun  3996  intpr  3997  disjiun  4120  brin  4178  brdif  4179  ssext  4356  pweqb  4358  opthg2  4374  copsex4g  4382  opelopabsb  4397  eqopab2b  4417  pwin  4422  pofun  4452  wetrep  4500  ordwe  4718  wessep  4720  reg3exmidlemwe  4721  elxp3  4824  soinxp  4840  relun  4889  inopab  4907  difopab  4908  inxp  4909  opelco2g  4943  cnvco  4960  dmin  4984  restidsing  5114  intasym  5167  asymref  5168  cnvdif  5189  xpm  5204  xp11m  5221  dfco2  5282  relssdmrn  5303  cnvpom  5325  xpcom  5329  dffun4  5383  dffun4f  5388  funun  5417  funcnveq  5439  fun11  5443  fununi  5444  imadif  5456  imainlem  5457  imain  5458  fnres  5495  fnopabg  5502  fun  5556  fin  5573  dff1o2  5639  brprcneu  5683  fsn  5871  dff1o6  5972  isotr  6012  brabvv  6124  eqoprab2b  6136  fvmpopr2d  6215  dfoprab3  6415  poxp  6458  cnvoprab  6460  f1od2  6461  brtpos2  6512  tfrlem7  6578  dfer2  6798  eqer  6829  iinerm  6871  brecop  6889  eroveu  6890  erovlem  6891  oviec  6905  mapval2  6949  ixpin  6995  modom  7098  xpcomco  7114  xpassen  7118  ssenen  7142  sbthlemi10  7273  infmoti  7358  dfmq0qs  7786  dfplq0qs  7787  enq0enq  7788  enq0tr  7791  npsspw  7828  nqprdisj  7901  ltnqpr  7950  ltnqpri  7951  ltexprlemdisj  7963  addcanprg  7973  recexprlemdisj  7987  caucvgprprlemval  8045  addsrpr  8102  mulsrpr  8103  mulgt0sr  8135  addcnsr  8191  mulcnsr  8192  ltresr  8196  addvalex  8201  axcnre  8238  axpre-suploc  8259  supinfneg  9974  infsupneg  9975  xrnemnf  10158  xrnepnf  10159  elfzuzb  10401  fzass4  10446  infssuzex  10644  hashfibclem  11260  hashfacen  11262  rexanre  11964  cbvprod  12303  nnwosdc  12794  isprm3  12874  issubm  13756  issubmd  13758  0subm  13768  insubm  13769  isnsg2  13983  lss1d  14692  tgval2  15075  epttop  15114  cnnei  15256  txuni2  15280  txbas  15282  txdis1cn  15302  xmeterval  15459  dedekindicc  15657  plyun0  15760  lgslem3  16035  vtxd0nedgbfi  16454  wlk1walkdom  16514  clwwlknonccat  16588  clwwlknon2x  16590  bj-stan  16689  nnti  16936