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  1410  merco2  1780  onint  7273  oalimcl  7924  oeordsuc  7958  fisup2g  8662  fiinf2g  8694  zorn2lem7  9659  inar1  9932  rpnnen1lem5  12128  expnbnd  13312  facwordi  13394  fi1uzind  13593  brfi1indALT  13596  unbenlem  16016  fiinopn  21113  cmpsublem  21611  dvcnvrelem1  24217  axcontlem4  26316  axcont  26325  spansncol  28999  atcvat4i  29828  sumdmdlem  29849  nocvxminlem  32482  broutsideof2  32818  relowlpssretop  33807  cvrat4  35597  pm2.43cbi  39678
  Copyright terms: Public domain W3C validator