MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an4 Structured version   Visualization version   GIF version

Theorem an4 655
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
an4 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))

Proof of Theorem an4
StepHypRef Expression
1 anass 470 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
2 an12 644 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
32bianass 641 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
41, 3bitri 275 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  an42  656  an4s  659  anandi  675  anandir  676  an6  1446  an33reanOLD  1485  reeanlem  3219  reu2  3688  rmo4  3693  rmo3f  3697  rmo3  3850  2reu1  3858  2reu4lem  4488  disjiun  5097  inxp  5793  xp11  6132  dfpo2  6253  fununi  6581  fun  6709  resoprab2  7480  sorpsscmpl  7676  xporderlem  8064  poxp  8065  poseq  8095  fprlem1  8236  frrlem15  9700  dfac5lem1  10066  zorn2lem6  10444  cju  12156  ixxin  13288  elfzo2  13582  xpcogend  14866  summo  15609  prodmo  15826  dfiso2  17662  issubmd  18624  gsumval3eu  19688  dvdsrtr  20088  isirred2  20139  lspsolvlem  20619  domnmuln0  20784  abvn0b  20788  unocv  21100  pf1ind  21737  ordtrest2lem  22570  lmmo  22747  ptbasin  22944  txbasval  22973  txcnp  22987  txlm  23015  tx1stc  23017  tx2ndc  23018  isfild  23225  txflf  23373  isclmp  24476  mbfi1flimlem  25103  iblcnlem1  25168  iblre  25174  iblcn  25179  logfaclbnd  26586  axcontlem4  27958  axcontlem7  27961  ocsh  30267  pjhthmo  30286  5oalem6  30643  cvnbtwn4  31273  superpos  31338  cdj3i  31425  13an22anass  31437  smatrcl  32417  ordtrest2NEWlem  32543  cusgr3cyclex  33770  lineext  34690  outsideoftr  34743  hilbert1.2  34769  lineintmo  34771  neibastop1  34860  bj-inrab  35426  isbasisrelowllem1  35855  isbasisrelowllem2  35856  ptrest  36106  poimirlem26  36133  ismblfin  36148  unirep  36201  inixp  36216  ablo4pnp  36368  keridl  36520  ispridlc  36558  anan  36713  disjecxrn  36880  coss1cnvres  36908  br1cosscnvxrn  36965  dfeldisj3  37210  antisymrelres  37254  prtlem70  37348  lcvbr3  37514  cvrnbtwn4  37770  linepsubN  38244  pmapsub  38260  pmapjoin  38344  ltrnu  38613  diblsmopel  39663  pell1234qrmulcl  41207  isdomn3  41560  ifpan23  41806  ifpidg  41837  ifpbibib  41856  uneqsn  42371  isthincd2  47132
  Copyright terms: Public domain W3C validator