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  1928  sbbi  1932  sbnf2  1956  eu1  2024  2exeu  2091  2eu4  2092  sbabel  2307  neanior  2395  rexeqbii  2448  r19.26m  2563  reean  2599  reu5  2643  reu2  2872  reu3  2874  eqss  3112  unss  3250  ralunb  3257  ssin  3298  undi  3324  difundi  3328  indifdir  3332  inab  3344  difab  3345  reuss2  3356  reupick  3360  raaan  3469  prss  3676  tpss  3685  prsspw  3692  prneimg  3701  uniin  3756  intun  3802  intpr  3803  disjiun  3924  brin  3980  brdif  3981  ssext  4143  pweqb  4145  opthg2  4161  copsex4g  4169  opelopabsb  4182  eqopab2b  4201  pwin  4204  pofun  4234  wetrep  4282  ordwe  4490  wessep  4492  reg3exmidlemwe  4493  elxp3  4593  soinxp  4609  relun  4656  inopab  4671  difopab  4672  inxp  4673  opelco2g  4707  cnvco  4724  dmin  4747  intasym  4923  asymref  4924  cnvdif  4945  xpm  4960  xp11m  4977  dfco2  5038  relssdmrn  5059  cnvpom  5081  xpcom  5085  dffun4  5134  dffun4f  5139  funun  5167  funcnveq  5186  fun11  5190  fununi  5191  imadif  5203  imainlem  5204  imain  5205  fnres  5239  fnopabg  5246  fun  5295  fin  5309  dff1o2  5372  brprcneu  5414  fsn  5592  dff1o6  5677  isotr  5717  brabvv  5817  eqoprab2b  5829  dfoprab3  6089  poxp  6129  cnvoprab  6131  f1od2  6132  brtpos2  6148  tfrlem7  6214  dfer2  6430  eqer  6461  iinerm  6501  brecop  6519  eroveu  6520  erovlem  6521  oviec  6535  mapval2  6572  ixpin  6617  xpcomco  6720  xpassen  6724  ssenen  6745  sbthlemi10  6854  infmoti  6915  dfmq0qs  7244  dfplq0qs  7245  enq0enq  7246  enq0tr  7249  npsspw  7286  nqprdisj  7359  ltnqpr  7408  ltnqpri  7409  ltexprlemdisj  7421  addcanprg  7431  recexprlemdisj  7445  caucvgprprlemval  7503  addsrpr  7560  mulsrpr  7561  mulgt0sr  7593  addcnsr  7649  mulcnsr  7650  ltresr  7654  addvalex  7659  axcnre  7696  axpre-suploc  7717  supinfneg  9397  infsupneg  9398  xrnemnf  9571  xrnepnf  9572  elfzuzb  9807  fzass4  9849  hashfacen  10586  rexanre  10999  cbvprod  11334  infssuzex  11649  isprm3  11806  tgval2  12230  epttop  12269  cnnei  12411  txuni2  12435  txbas  12437  txdis1cn  12457  xmeterval  12614  dedekindicc  12790  bj-stan  12965  nnti  13201