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  1349  merco2  1739  onint  7778  oalimcl  8560  oeordsuc  8594  fisup2g  9463  fiinf2g  9495  zorn2lem7  10497  inar1  10770  rpnnen1lem5  12965  expnbnd  14195  facwordi  14249  fi1uzind  14458  brfi1indALT  14461  unbenlem  16841  fiinopn  22403  cmpsublem  22903  dvcnvrelem1  25534  nocvxminlem  27279  axcontlem4  28225  axcont  28234  spansncol  30821  atcvat4i  31650  sumdmdlem  31671  broutsideof2  35094  relowlpssretop  36245  cvrat4  38314  pm2.43cbi  43279
  Copyright terms: Public domain W3C validator