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  1346  merco2  1731  onint  7787  oalimcl  8574  oeordsuc  8608  fisup2g  9483  fiinf2g  9515  zorn2lem7  10517  inar1  10790  rpnnen1lem5  12987  expnbnd  14218  facwordi  14272  fi1uzind  14482  brfi1indALT  14485  unbenlem  16868  fiinopn  22790  cmpsublem  23290  dvcnvrelem1  25937  nocvxminlem  27697  axcontlem4  28765  axcont  28774  spansncol  31365  atcvat4i  32194  sumdmdlem  32215  broutsideof2  35654  relowlpssretop  36779  cvrat4  38853  pm2.43cbi  43880
  Copyright terms: Public domain W3C validator