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  1939  sban  2009  sbbi  2013  sbnf2  2035  eu1  2105  2exeu  2173  2eu4  2174  sbabel  2411  neanior  2499  rexeqbii  2555  r19.26m  2674  reean  2712  reu5  2762  cbvreuw  2773  reu2  3005  reu3  3007  eqss  3253  unss  3393  ralunb  3400  ssin  3443  undi  3469  difundi  3473  indifdir  3477  inab  3489  difab  3490  reuss2  3501  reupick  3505  raaan  3615  prss  3850  tpss  3862  prsspw  3869  prneimg  3878  uniin  3934  intun  3980  intpr  3981  disjiun  4104  brin  4162  brdif  4163  ssext  4337  pweqb  4339  opthg2  4355  copsex4g  4363  opelopabsb  4378  eqopab2b  4398  pwin  4403  pofun  4433  wetrep  4481  ordwe  4698  wessep  4700  reg3exmidlemwe  4701  elxp3  4804  soinxp  4820  relun  4869  inopab  4887  difopab  4888  inxp  4889  opelco2g  4923  cnvco  4940  dmin  4964  restidsing  5094  intasym  5147  asymref  5148  cnvdif  5169  xpm  5184  xp11m  5201  dfco2  5262  relssdmrn  5283  cnvpom  5305  xpcom  5309  dffun4  5363  dffun4f  5368  funun  5397  funcnveq  5419  fun11  5423  fununi  5424  imadif  5436  imainlem  5437  imain  5438  fnres  5475  fnopabg  5482  fun  5536  fin  5553  dff1o2  5619  brprcneu  5663  fsn  5849  dff1o6  5949  isotr  5989  brabvv  6099  eqoprab2b  6111  fvmpopr2d  6190  dfoprab3  6385  poxp  6428  cnvoprab  6430  f1od2  6431  brtpos2  6482  tfrlem7  6548  dfer2  6768  eqer  6799  iinerm  6841  brecop  6859  eroveu  6860  erovlem  6861  oviec  6875  mapval2  6912  ixpin  6958  modom  7061  xpcomco  7077  xpassen  7081  ssenen  7105  sbthlemi10  7236  infmoti  7319  dfmq0qs  7744  dfplq0qs  7745  enq0enq  7746  enq0tr  7749  npsspw  7786  nqprdisj  7859  ltnqpr  7908  ltnqpri  7909  ltexprlemdisj  7921  addcanprg  7931  recexprlemdisj  7945  caucvgprprlemval  8003  addsrpr  8060  mulsrpr  8061  mulgt0sr  8093  addcnsr  8149  mulcnsr  8150  ltresr  8154  addvalex  8159  axcnre  8196  axpre-suploc  8217  supinfneg  9927  infsupneg  9928  xrnemnf  10110  xrnepnf  10111  elfzuzb  10353  fzass4  10396  infssuzex  10593  hashfibclem  11206  hashfacen  11208  rexanre  11905  cbvprod  12244  nnwosdc  12735  isprm3  12815  issubm  13685  issubmd  13687  0subm  13697  insubm  13698  isnsg2  13920  lss1d  14531  tgval2  14916  epttop  14955  cnnei  15097  txuni2  15121  txbas  15123  txdis1cn  15143  xmeterval  15300  dedekindicc  15498  plyun0  15601  lgslem3  15875  vtxd0nedgbfi  16294  wlk1walkdom  16354  clwwlknonccat  16428  clwwlknon2x  16430  bj-stan  16519  nnti  16766