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  819  orddi  822  3anbi123i  1191  an6  1334  xorcom  1408  trubifal  1436  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  nford  1591  nfand  1592  sbequ8  1871  sbanv  1914  sban  1984  sbbi  1988  sbnf2  2010  eu1  2080  2exeu  2148  2eu4  2149  sbabel  2377  neanior  2465  rexeqbii  2521  r19.26m  2639  reean  2677  reu5  2726  cbvreuw  2737  reu2  2968  reu3  2970  eqss  3216  unss  3355  ralunb  3362  ssin  3403  undi  3429  difundi  3433  indifdir  3437  inab  3449  difab  3450  reuss2  3461  reupick  3465  raaan  3574  prss  3800  tpss  3812  prsspw  3819  prneimg  3828  uniin  3884  intun  3930  intpr  3931  disjiun  4054  brin  4112  brdif  4113  ssext  4283  pweqb  4285  opthg2  4301  copsex4g  4309  opelopabsb  4324  eqopab2b  4344  pwin  4347  pofun  4377  wetrep  4425  ordwe  4642  wessep  4644  reg3exmidlemwe  4645  elxp3  4747  soinxp  4763  relun  4810  inopab  4828  difopab  4829  inxp  4830  opelco2g  4864  cnvco  4881  dmin  4905  restidsing  5034  intasym  5086  asymref  5087  cnvdif  5108  xpm  5123  xp11m  5140  dfco2  5201  relssdmrn  5222  cnvpom  5244  xpcom  5248  dffun4  5301  dffun4f  5306  funun  5334  funcnveq  5356  fun11  5360  fununi  5361  imadif  5373  imainlem  5374  imain  5375  fnres  5412  fnopabg  5419  fun  5469  fin  5484  dff1o2  5549  brprcneu  5592  fsn  5775  dff1o6  5868  isotr  5908  brabvv  6014  eqoprab2b  6026  fvmpopr2d  6105  dfoprab3  6300  poxp  6341  cnvoprab  6343  f1od2  6344  brtpos2  6360  tfrlem7  6426  dfer2  6644  eqer  6675  iinerm  6717  brecop  6735  eroveu  6736  erovlem  6737  oviec  6751  mapval2  6788  ixpin  6833  xpcomco  6946  xpassen  6950  ssenen  6973  sbthlemi10  7094  infmoti  7156  dfmq0qs  7577  dfplq0qs  7578  enq0enq  7579  enq0tr  7582  npsspw  7619  nqprdisj  7692  ltnqpr  7741  ltnqpri  7742  ltexprlemdisj  7754  addcanprg  7764  recexprlemdisj  7778  caucvgprprlemval  7836  addsrpr  7893  mulsrpr  7894  mulgt0sr  7926  addcnsr  7982  mulcnsr  7983  ltresr  7987  addvalex  7992  axcnre  8029  axpre-suploc  8050  supinfneg  9751  infsupneg  9752  xrnemnf  9934  xrnepnf  9935  elfzuzb  10176  fzass4  10219  infssuzex  10413  hashfacen  11018  rexanre  11646  cbvprod  11984  nnwosdc  12475  isprm3  12555  issubm  13419  issubmd  13421  0subm  13431  insubm  13432  isnsg2  13654  lss1d  14260  tgval2  14638  epttop  14677  cnnei  14819  txuni2  14843  txbas  14845  txdis1cn  14865  xmeterval  15022  dedekindicc  15220  plyun0  15323  lgslem3  15594  bj-stan  15883  nnti  16129