Theorem anbi12i 447

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

Syntax hints:   ∧ wa 102   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi12ci  448  ordir  763  orddi  766  dcan  875  3anbi123i  1127  an6  1252  xorcom  1319  trubifal  1347  truxortru  1350  truxorfal  1351  falxortru  1352  falxorfal  1353  nford  1499  nfand  1500  sbequ8  1768  sbanv  1810  sban  1870  sbbi  1874  sbnf2  1898  eu1  1966  2exeu  2033  2eu4  2034  sbabel  2244  neanior  2332  rexeqbii  2379  r19.26m  2488  reean  2522  reu5  2566  reu2  2780  reu3  2782  eqss  3014  unss  3146  ralunb  3153  ssin  3188  undi  3212  difundi  3216  indifdir  3220  inab  3232  difab  3233  reuss2  3244  reupick  3248  raaan  3347  prss  3541  tpss  3550  prsspw  3557  prneimg  3566  uniin  3621  intun  3667  intpr  3668  brin  3832  brdif  3833  ssext  3976  pweqb  3978  opthg2  3994  copsex4g  4002  opelopabsb  4015  eqopab2b  4034  pwin  4037  pofun  4067  wetrep  4115  ordwe  4318  wessep  4320  reg3exmidlemwe  4321  elxp3  4412  soinxp  4428  relun  4472  inopab  4486  difopab  4487  inxp  4488  opelco2g  4521  cnvco  4538  dmin  4561  intasym  4729  asymref  4730  cnvdif  4750  xpm  4765  xp11m  4779  dfco2  4840  relssdmrn  4861  cnvpom  4880  xpcom  4884  dffun4  4933  dffun4f  4938  funun  4964  funcnveq  4982  fun11  4986  fununi  4987  imadif  4999  imainlem  5000  imain  5001  fnres  5035  fnopabg  5042  fun  5083  fin  5096  dff1o2  5151  brprcneu  5191  fsn  5356  dff1o6  5436  isotr  5476  brabvv  5571  eqoprab2b  5583  dfoprab3  5837  poxp  5873  cnvoprab  5875  f1od2  5876  brtpos2  5889  tfrlem7  5956  dfer2  6130  eqer  6161  iinerm  6201  brecop  6219  eroveu  6220  erovlem  6221  oviec  6235  xpcomco  6323  xpassen  6327  infmoti  6441  dfmq0qs  6619  dfplq0qs  6620  enq0enq  6621  enq0tr  6624  npsspw  6661  nqprdisj  6734  ltnqpr  6783  ltnqpri  6784  ltexprlemdisj  6796  addcanprg  6806  recexprlemdisj  6820  caucvgprprlemval  6878  addsrpr  6922  mulsrpr  6923  mulgt0sr  6954  addcnsr  7002  mulcnsr  7003  ltresr  7007  addvalex  7012  axcnre  7047  supinfneg  8683  infsupneg  8684  xrnemnf  8853  xrnepnf  8854  elfzuzb  9039  fzass4  9080  rexanre  10106  infssuzex  10345  isprm3  10500