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  7793  oalimcl  8581  oeordsuc  8615  fisup2g  9492  fiinf2g  9524  zorn2lem7  10526  inar1  10799  rpnnen1lem5  12996  expnbnd  14227  facwordi  14281  fi1uzind  14491  brfi1indALT  14494  unbenlem  16877  fiinopn  22816  cmpsublem  23316  dvcnvrelem1  25963  nocvxminlem  27723  axcontlem4  28791  axcont  28800  spansncol  31391  atcvat4i  32220  sumdmdlem  32241  broutsideof2  35718  relowlpssretop  36843  cvrat4  38916  pm2.43cbi  43957
  Copyright terms: Public domain W3C validator