Theorem anbi12i 455

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 453	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 452	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 183	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12ci  456  ordir  806  orddi  809  dcan  918  3anbi123i  1170  an6  1299  xorcom  1366  trubifal  1394  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  nford  1546  nfand  1547  sbequ8  1819  sbanv  1861  sban  1926  sbbi  1930  sbnf2  1954  eu1  2022  2exeu  2089  2eu4  2090  sbabel  2305  neanior  2393  rexeqbii  2446  r19.26m  2561  reean  2597  reu5  2641  reu2  2867  reu3  2869  eqss  3107  unss  3245  ralunb  3252  ssin  3293  undi  3319  difundi  3323  indifdir  3327  inab  3339  difab  3340  reuss2  3351  reupick  3355  raaan  3464  prss  3671  tpss  3680  prsspw  3687  prneimg  3696  uniin  3751  intun  3797  intpr  3798  disjiun  3919  brin  3975  brdif  3976  ssext  4138  pweqb  4140  opthg2  4156  copsex4g  4164  opelopabsb  4177  eqopab2b  4196  pwin  4199  pofun  4229  wetrep  4277  ordwe  4485  wessep  4487  reg3exmidlemwe  4488  elxp3  4588  soinxp  4604  relun  4651  inopab  4666  difopab  4667  inxp  4668  opelco2g  4702  cnvco  4719  dmin  4742  intasym  4918  asymref  4919  cnvdif  4940  xpm  4955  xp11m  4972  dfco2  5033  relssdmrn  5054  cnvpom  5076  xpcom  5080  dffun4  5129  dffun4f  5134  funun  5162  funcnveq  5181  fun11  5185  fununi  5186  imadif  5198  imainlem  5199  imain  5200  fnres  5234  fnopabg  5241  fun  5290  fin  5304  dff1o2  5365  brprcneu  5407  fsn  5585  dff1o6  5670  isotr  5710  brabvv  5810  eqoprab2b  5822  dfoprab3  6082  poxp  6122  cnvoprab  6124  f1od2  6125  brtpos2  6141  tfrlem7  6207  dfer2  6423  eqer  6454  iinerm  6494  brecop  6512  eroveu  6513  erovlem  6514  oviec  6528  mapval2  6565  ixpin  6610  xpcomco  6713  xpassen  6717  ssenen  6738  sbthlemi10  6847  infmoti  6908  dfmq0qs  7230  dfplq0qs  7231  enq0enq  7232  enq0tr  7235  npsspw  7272  nqprdisj  7345  ltnqpr  7394  ltnqpri  7395  ltexprlemdisj  7407  addcanprg  7417  recexprlemdisj  7431  caucvgprprlemval  7489  addsrpr  7546  mulsrpr  7547  mulgt0sr  7579  addcnsr  7635  mulcnsr  7636  ltresr  7640  addvalex  7645  axcnre  7682  axpre-suploc  7703  supinfneg  9383  infsupneg  9384  xrnemnf  9557  xrnepnf  9558  elfzuzb  9793  fzass4  9835  hashfacen  10572  rexanre  10985  cbvprod  11320  infssuzex  11631  isprm3  11788  tgval2  12209  epttop  12248  cnnei  12390  txuni2  12414  txbas  12416  txdis1cn  12436  xmeterval  12593  dedekindicc  12769  bj-stan  12944  nnti  13180