Theorem anbi12i 453

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12ci  454  ordir  789  orddi  792  dcan  901  3anbi123i  1153  an6  1282  xorcom  1349  trubifal  1377  truxortru  1380  truxorfal  1381  falxortru  1382  falxorfal  1383  nford  1529  nfand  1530  sbequ8  1801  sbanv  1843  sban  1904  sbbi  1908  sbnf2  1932  eu1  2000  2exeu  2067  2eu4  2068  sbabel  2281  neanior  2369  rexeqbii  2422  r19.26m  2537  reean  2573  reu5  2617  reu2  2841  reu3  2843  eqss  3078  unss  3216  ralunb  3223  ssin  3264  undi  3290  difundi  3294  indifdir  3298  inab  3310  difab  3311  reuss2  3322  reupick  3326  raaan  3435  prss  3642  tpss  3651  prsspw  3658  prneimg  3667  uniin  3722  intun  3768  intpr  3769  disjiun  3890  brin  3942  brdif  3943  ssext  4103  pweqb  4105  opthg2  4121  copsex4g  4129  opelopabsb  4142  eqopab2b  4161  pwin  4164  pofun  4194  wetrep  4242  ordwe  4450  wessep  4452  reg3exmidlemwe  4453  elxp3  4553  soinxp  4569  relun  4616  inopab  4631  difopab  4632  inxp  4633  opelco2g  4667  cnvco  4684  dmin  4707  intasym  4881  asymref  4882  cnvdif  4903  xpm  4918  xp11m  4935  dfco2  4996  relssdmrn  5017  cnvpom  5039  xpcom  5043  dffun4  5092  dffun4f  5097  funun  5125  funcnveq  5144  fun11  5148  fununi  5149  imadif  5161  imainlem  5162  imain  5163  fnres  5197  fnopabg  5204  fun  5253  fin  5267  dff1o2  5328  brprcneu  5368  fsn  5546  dff1o6  5631  isotr  5671  brabvv  5771  eqoprab2b  5783  dfoprab3  6043  poxp  6083  cnvoprab  6085  f1od2  6086  brtpos2  6102  tfrlem7  6168  dfer2  6384  eqer  6415  iinerm  6455  brecop  6473  eroveu  6474  erovlem  6475  oviec  6489  mapval2  6526  ixpin  6571  xpcomco  6673  xpassen  6677  ssenen  6698  sbthlemi10  6806  infmoti  6867  dfmq0qs  7185  dfplq0qs  7186  enq0enq  7187  enq0tr  7190  npsspw  7227  nqprdisj  7300  ltnqpr  7349  ltnqpri  7350  ltexprlemdisj  7362  addcanprg  7372  recexprlemdisj  7386  caucvgprprlemval  7444  addsrpr  7488  mulsrpr  7489  mulgt0sr  7520  addcnsr  7569  mulcnsr  7570  ltresr  7574  addvalex  7579  axcnre  7616  supinfneg  9292  infsupneg  9293  xrnemnf  9457  xrnepnf  9458  elfzuzb  9693  fzass4  9735  hashfacen  10472  rexanre  10884  infssuzex  11490  isprm3  11645  tgval2  12063  epttop  12102  cnnei  12243  txuni2  12267  txbas  12269  txdis1cn  12289  xmeterval  12424  bj-stan  12648  nnti  12883