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  2991  reu3  2993  eqss  3239  unss  3378  ralunb  3385  ssin  3426  undi  3452  difundi  3456  indifdir  3460  inab  3472  difab  3473  reuss2  3484  reupick  3488  raaan  3597  prss  3824  tpss  3836  prsspw  3843  prneimg  3852  uniin  3908  intun  3954  intpr  3955  disjiun  4078  brin  4136  brdif  4137  ssext  4307  pweqb  4309  opthg2  4325  copsex4g  4333  opelopabsb  4348  eqopab2b  4368  pwin  4373  pofun  4403  wetrep  4451  ordwe  4668  wessep  4670  reg3exmidlemwe  4671  elxp3  4773  soinxp  4789  relun  4836  inopab  4854  difopab  4855  inxp  4856  opelco2g  4890  cnvco  4907  dmin  4931  restidsing  5061  intasym  5113  asymref  5114  cnvdif  5135  xpm  5150  xp11m  5167  dfco2  5228  relssdmrn  5249  cnvpom  5271  xpcom  5275  dffun4  5329  dffun4f  5334  funun  5362  funcnveq  5384  fun11  5388  fununi  5389  imadif  5401  imainlem  5402  imain  5403  fnres  5440  fnopabg  5447  fun  5499  fin  5514  dff1o2  5579  brprcneu  5622  fsn  5809  dff1o6  5906  isotr  5946  brabvv  6056  eqoprab2b  6068  fvmpopr2d  6147  dfoprab3  6343  poxp  6384  cnvoprab  6386  f1od2  6387  brtpos2  6403  tfrlem7  6469  dfer2  6689  eqer  6720  iinerm  6762  brecop  6780  eroveu  6781  erovlem  6782  oviec  6796  mapval2  6833  ixpin  6878  xpcomco  6993  xpassen  6997  ssenen  7020  sbthlemi10  7144  infmoti  7206  dfmq0qs  7627  dfplq0qs  7628  enq0enq  7629  enq0tr  7632  npsspw  7669  nqprdisj  7742  ltnqpr  7791  ltnqpri  7792  ltexprlemdisj  7804  addcanprg  7814  recexprlemdisj  7828  caucvgprprlemval  7886  addsrpr  7943  mulsrpr  7944  mulgt0sr  7976  addcnsr  8032  mulcnsr  8033  ltresr  8037  addvalex  8042  axcnre  8079  axpre-suploc  8100  supinfneg  9802  infsupneg  9803  xrnemnf  9985  xrnepnf  9986  elfzuzb  10227  fzass4  10270  infssuzex  10465  hashfacen  11071  rexanre  11746  cbvprod  12084  nnwosdc  12575  isprm3  12655  issubm  13520  issubmd  13522  0subm  13532  insubm  13533  isnsg2  13755  lss1d  14362  tgval2  14740  epttop  14779  cnnei  14921  txuni2  14945  txbas  14947  txdis1cn  14967  xmeterval  15124  dedekindicc  15322  plyun0  15425  lgslem3  15696  wlk1walkdom  16100  bj-stan  16166  nnti  16415