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

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

Proof of Theorem an4
StepHypRef Expression
1 anass 469 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
2 an12 641 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
32bianass 638 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
41, 3bitri 276 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  an42  653  an4s  656  anandi  672  anandir  673  an6  1438  an33rean  1476  reeanlem  3371  reu2  3720  rmo4  3725  rmo3f  3729  rmo3  3876  rmo3OLD  3877  2reu1  3885  2reu4lem  4468  disjiun  5050  inxp  5702  xp11  6031  fununi  6428  fun  6539  resoprab2  7265  sorpsscmpl  7454  xporderlem  7817  poxp  7818  dfac5lem1  9543  zorn2lem6  9917  cju  11628  ixxin  12750  elfzo2  13036  xpcogend  14329  summo  15069  prodmo  15285  dfiso2  17037  issubmd  17966  gsumval3eu  18960  dvdsrtr  19338  isirred2  19387  lspsolvlem  19850  domnmuln0  20006  abvn0b  20010  pf1ind  20453  unocv  20759  ordtrest2lem  21746  lmmo  21923  ptbasin  22120  txbasval  22149  txcnp  22163  txlm  22191  tx1stc  22193  tx2ndc  22194  isfild  22401  txflf  22549  isclmp  23635  mbfi1flimlem  24257  iblcnlem1  24322  iblre  24328  iblcn  24333  logfaclbnd  25731  axcontlem4  26686  axcontlem7  26689  ocsh  28993  pjhthmo  29012  5oalem6  29369  cvnbtwn4  29999  superpos  30064  cdj3i  30151  smatrcl  30966  ordtrest2NEWlem  31070  cusgr3cyclex  32286  dfpo2  32894  poseq  32998  fprlem1  33040  frrlem15  33045  lineext  33440  outsideoftr  33493  hilbert1.2  33519  lineintmo  33521  neibastop1  33610  bj-inrab  34148  isbasisrelowllem1  34524  isbasisrelowllem2  34525  ptrest  34777  poimirlem26  34804  ismblfin  34819  unirep  34875  inixp  34890  ablo4pnp  35045  keridl  35197  ispridlc  35235  anan  35386  br1cosscnvxrn  35600  dfeldisj3  35838  prtlem70  35879  lcvbr3  36045  cvrnbtwn4  36301  linepsubN  36774  pmapsub  36790  pmapjoin  36874  ltrnu  37143  diblsmopel  38193  pell1234qrmulcl  39336  isdomn3  39688  ifpan23  39709  ifpidg  39741  ifpbibib  39760  uneqsn  40257
  Copyright terms: Public domain W3C validator