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

Theorem com4l 92
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.)
Hypothesis
Ref Expression
com4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com4l (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))

Proof of Theorem com4l
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com3l 89 . 2 (𝜓 → (𝜒 → (𝜑 → (𝜃𝜏))))
32com34 91 1 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com4t  93  com4r  94  com14  96  com5l  100  3impd  1348  merco2  1738  onint  7780  oalimcl  8562  oeordsuc  8596  fisup2g  9465  fiinf2g  9497  zorn2lem7  10499  inar1  10772  rpnnen1lem5  12967  expnbnd  14197  facwordi  14251  fi1uzind  14460  brfi1indALT  14463  unbenlem  16843  fiinopn  22410  cmpsublem  22910  dvcnvrelem1  25541  nocvxminlem  27286  axcontlem4  28263  axcont  28272  spansncol  30859  atcvat4i  31688  sumdmdlem  31709  broutsideof2  35169  relowlpssretop  36337  cvrat4  38406  pm2.43cbi  43367
  Copyright terms: Public domain W3C validator