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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 873 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 732 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 684 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 684 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 292 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  an42  901  an4s  904  anandi  906  anandir  907  an6  1555  an33rean  1593  reean  3242  reu2  3533  rmo4  3538  rmo3  3667  disjiun  4790  inxp  5408  xp11  5725  fununi  6123  fun  6225  resoprab2  6920  sorpsscmpl  7111  xporderlem  7454  poxp  7455  dfac5lem1  9134  zorn2lem6  9513  cju  11206  ixxin  12383  elfzo2  12665  xpcogend  13912  summo  14645  prodmo  14863  dfiso2  16631  issubmd  17548  gsumval3eu  18503  dvdsrtr  18850  isirred2  18899  lspsolvlem  19342  domnmuln0  19498  abvn0b  19502  pf1ind  19919  unocv  20224  ordtrest2lem  21207  lmmo  21384  ptbasin  21580  txbasval  21609  txcnp  21623  txlm  21651  tx1stc  21653  tx2ndc  21654  isfild  21861  txflf  22009  isclmp  23095  mbfi1flimlem  23686  iblcnlem1  23751  iblre  23757  iblcn  23762  logfaclbnd  25144  axcontlem4  26044  axcontlem7  26047  ocsh  28449  pjhthmo  28468  5oalem6  28825  cvnbtwn4  29455  superpos  29520  cdj3i  29607  rmo3f  29641  rmo4fOLD  29642  smatrcl  30169  ordtrest2NEWlem  30275  dfpo2  31950  poseq  32057  lineext  32487  outsideoftr  32540  hilbert1.2  32566  lineintmo  32568  neibastop1  32658  bj-inrab  33227  isbasisrelowllem1  33512  isbasisrelowllem2  33513  ptrest  33719  poimirlem26  33746  ismblfin  33761  unirep  33818  inixp  33834  ablo4pnp  33990  keridl  34142  ispridlc  34180  anan  34323  br1cosscnvxrn  34545  prtlem70  34643  lcvbr3  34811  cvrnbtwn4  35067  linepsubN  35539  pmapsub  35555  pmapjoin  35639  ltrnu  35908  diblsmopel  36960  pell1234qrmulcl  37919  isdomn3  38282  ifpan23  38304  ifpidg  38336  ifpbibib  38355  uneqsn  38821  2reu1  41690  2reu4a  41693
  Copyright terms: Public domain W3C validator