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  822  orddi  825  3anbi123i  1212  an6  1355  xorcom  1430  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  nford  1613  nfand  1614  sbequ8  1893  sbanv  1936  sban  2006  sbbi  2010  sbnf2  2032  eu1  2102  2exeu  2170  2eu4  2171  sbabel  2399  neanior  2487  rexeqbii  2543  r19.26m  2662  reean  2700  reu5  2749  cbvreuw  2760  reu2  2992  reu3  2994  eqss  3240  unss  3379  ralunb  3386  ssin  3427  undi  3453  difundi  3457  indifdir  3461  inab  3473  difab  3474  reuss2  3485  reupick  3489  raaan  3598  prss  3827  tpss  3839  prsspw  3846  prneimg  3855  uniin  3911  intun  3957  intpr  3958  disjiun  4081  brin  4139  brdif  4140  ssext  4311  pweqb  4313  opthg2  4329  copsex4g  4337  opelopabsb  4352  eqopab2b  4372  pwin  4377  pofun  4407  wetrep  4455  ordwe  4672  wessep  4674  reg3exmidlemwe  4675  elxp3  4778  soinxp  4794  relun  4842  inopab  4860  difopab  4861  inxp  4862  opelco2g  4896  cnvco  4913  dmin  4937  restidsing  5067  intasym  5119  asymref  5120  cnvdif  5141  xpm  5156  xp11m  5173  dfco2  5234  relssdmrn  5255  cnvpom  5277  xpcom  5281  dffun4  5335  dffun4f  5340  funun  5368  funcnveq  5390  fun11  5394  fununi  5395  imadif  5407  imainlem  5408  imain  5409  fnres  5446  fnopabg  5453  fun  5505  fin  5520  dff1o2  5585  brprcneu  5628  fsn  5815  dff1o6  5912  isotr  5952  brabvv  6062  eqoprab2b  6074  fvmpopr2d  6153  dfoprab3  6349  poxp  6392  cnvoprab  6394  f1od2  6395  brtpos2  6412  tfrlem7  6478  dfer2  6698  eqer  6729  iinerm  6771  brecop  6789  eroveu  6790  erovlem  6791  oviec  6805  mapval2  6842  ixpin  6887  modom  6989  xpcomco  7005  xpassen  7009  ssenen  7032  sbthlemi10  7156  infmoti  7218  dfmq0qs  7639  dfplq0qs  7640  enq0enq  7641  enq0tr  7644  npsspw  7681  nqprdisj  7754  ltnqpr  7803  ltnqpri  7804  ltexprlemdisj  7816  addcanprg  7826  recexprlemdisj  7840  caucvgprprlemval  7898  addsrpr  7955  mulsrpr  7956  mulgt0sr  7988  addcnsr  8044  mulcnsr  8045  ltresr  8049  addvalex  8054  axcnre  8091  axpre-suploc  8112  supinfneg  9819  infsupneg  9820  xrnemnf  10002  xrnepnf  10003  elfzuzb  10244  fzass4  10287  infssuzex  10483  hashfacen  11090  rexanre  11771  cbvprod  12109  nnwosdc  12600  isprm3  12680  issubm  13545  issubmd  13547  0subm  13557  insubm  13558  isnsg2  13780  lss1d  14387  tgval2  14765  epttop  14804  cnnei  14946  txuni2  14970  txbas  14972  txdis1cn  14992  xmeterval  15149  dedekindicc  15347  plyun0  15450  lgslem3  15721  vtxd0nedgbfi  16105  wlk1walkdom  16156  clwwlknonccat  16228  clwwlknon2x  16230  bj-stan  16279  nnti  16527