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  825  orddi  828  3anbi123i  1215  an6  1358  xorcom  1433  trubifal  1461  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  nford  1616  nfand  1617  sbequ8  1896  sbanv  1940  sban  2011  sbbi  2015  sbnf2  2037  eu1  2107  2exeu  2175  2eu4  2176  sbabel  2413  neanior  2501  rexeqbii  2557  r19.26m  2676  reean  2714  reu5  2764  cbvreuw  2775  reu2  3008  reu3  3010  eqss  3257  unss  3397  ralunb  3404  ssin  3447  undi  3473  difundi  3477  indifdir  3481  inab  3493  difab  3494  reuss2  3505  reupick  3509  raaan  3619  prss  3855  tpss  3867  prsspw  3874  prneimg  3883  uniin  3939  intun  3985  intpr  3986  disjiun  4109  brin  4167  brdif  4168  ssext  4342  pweqb  4344  opthg2  4360  copsex4g  4368  opelopabsb  4383  eqopab2b  4403  pwin  4408  pofun  4438  wetrep  4486  ordwe  4703  wessep  4705  reg3exmidlemwe  4706  elxp3  4809  soinxp  4825  relun  4874  inopab  4892  difopab  4893  inxp  4894  opelco2g  4928  cnvco  4945  dmin  4969  restidsing  5099  intasym  5152  asymref  5153  cnvdif  5174  xpm  5189  xp11m  5206  dfco2  5267  relssdmrn  5288  cnvpom  5310  xpcom  5314  dffun4  5368  dffun4f  5373  funun  5402  funcnveq  5424  fun11  5428  fununi  5429  imadif  5441  imainlem  5442  imain  5443  fnres  5480  fnopabg  5487  fun  5541  fin  5558  dff1o2  5624  brprcneu  5668  fsn  5854  dff1o6  5955  isotr  5995  brabvv  6107  eqoprab2b  6119  fvmpopr2d  6198  dfoprab3  6398  poxp  6441  cnvoprab  6443  f1od2  6444  brtpos2  6495  tfrlem7  6561  dfer2  6781  eqer  6812  iinerm  6854  brecop  6872  eroveu  6873  erovlem  6874  oviec  6888  mapval2  6925  ixpin  6971  modom  7074  xpcomco  7090  xpassen  7094  ssenen  7118  sbthlemi10  7249  infmoti  7332  dfmq0qs  7760  dfplq0qs  7761  enq0enq  7762  enq0tr  7765  npsspw  7802  nqprdisj  7875  ltnqpr  7924  ltnqpri  7925  ltexprlemdisj  7937  addcanprg  7947  recexprlemdisj  7961  caucvgprprlemval  8019  addsrpr  8076  mulsrpr  8077  mulgt0sr  8109  addcnsr  8165  mulcnsr  8166  ltresr  8170  addvalex  8175  axcnre  8212  axpre-suploc  8233  supinfneg  9945  infsupneg  9946  xrnemnf  10129  xrnepnf  10130  elfzuzb  10372  fzass4  10417  infssuzex  10615  hashfibclem  11231  hashfacen  11233  rexanre  11930  cbvprod  12269  nnwosdc  12760  isprm3  12840  issubm  13727  issubmd  13729  0subm  13739  insubm  13740  isnsg2  13956  lss1d  14657  tgval2  15042  epttop  15081  cnnei  15223  txuni2  15247  txbas  15249  txdis1cn  15269  xmeterval  15426  dedekindicc  15624  plyun0  15727  lgslem3  16001  vtxd0nedgbfi  16420  wlk1walkdom  16480  clwwlknonccat  16554  clwwlknon2x  16556  bj-stan  16645  nnti  16892