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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 635 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 616 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 460 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 460 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 294 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  an42  647  an4s  650  anandi  666  anandir  667  an6  1569  an33rean  1607  reean  3253  reu2  3553  rmo4  3558  rmo3f  3562  rmo3  3686  disjiun  4797  inxp  5423  xp11  5752  fununi  6142  fun  6248  resoprab2  6955  sorpsscmpl  7146  xporderlem  7490  poxp  7491  dfac5lem1  9197  zorn2lem6  9576  cju  11270  ixxin  12394  elfzo2  12681  xpcogend  14000  summo  14733  prodmo  14949  dfiso2  16697  issubmd  17615  gsumval3eu  18571  dvdsrtr  18919  isirred2  18968  lspsolvlem  19415  domnmuln0  19572  abvn0b  19576  pf1ind  19992  unocv  20300  ordtrest2lem  21287  lmmo  21464  ptbasin  21660  txbasval  21689  txcnp  21703  txlm  21731  tx1stc  21733  tx2ndc  21734  isfild  21941  txflf  22089  isclmp  23175  mbfi1flimlem  23780  iblcnlem1  23845  iblre  23851  iblcn  23856  logfaclbnd  25238  axcontlem4  26138  axcontlem7  26141  ocsh  28598  pjhthmo  28617  5oalem6  28974  cvnbtwn4  29604  superpos  29669  cdj3i  29756  smatrcl  30309  ordtrest2NEWlem  30415  dfpo2  32090  poseq  32197  lineext  32627  outsideoftr  32680  hilbert1.2  32706  lineintmo  32708  neibastop1  32797  bj-inrab  33351  isbasisrelowllem1  33636  isbasisrelowllem2  33637  ptrest  33832  poimirlem26  33859  ismblfin  33874  unirep  33930  inixp  33946  ablo4pnp  34101  keridl  34253  ispridlc  34291  anan  34436  br1cosscnvxrn  34653  prtlem70  34812  lcvbr3  34979  cvrnbtwn4  35235  linepsubN  35708  pmapsub  35724  pmapjoin  35808  ltrnu  36077  diblsmopel  37127  pell1234qrmulcl  38097  isdomn3  38459  ifpan23  38480  ifpidg  38512  ifpbibib  38531  uneqsn  38995  2reu1  41857  2reu4a  41860
  Copyright terms: Public domain W3C validator