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

Theorem com4l 90
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 87 . 2 (𝜓 → (𝜒 → (𝜑 → (𝜃𝜏))))
32com34 89 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  91  com4r  92  com14  94  com5l  98  3impd  1273  merco2  1652  onint  6865  oalimcl  7505  oeordsuc  7539  fisup2g  8235  fiinf2g  8267  zorn2lem7  9185  inar1  9454  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  expnbnd  12813  facwordi  12896  fi1uzind  13083  brfi1indALT  13086  fi1uzindOLD  13089  brfi1indALTOLD  13092  unbenlem  15399  fiinopn  20479  cmpsublem  20960  dvcnvrelem1  23529  axcontlem4  25593  axcont  25602  spansncol  27605  atcvat4i  28434  sumdmdlem  28455  nocvxminlem  30883  broutsideof2  31193  relowlpssretop  32182  cvrat4  33541  pm2.43cbi  37539
  Copyright terms: Public domain W3C validator