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  1345  merco2  1738  onint  7495  oalimcl  8173  oeordsuc  8207  fisup2g  8920  fiinf2g  8952  zorn2lem7  9913  inar1  10186  rpnnen1lem5  12368  expnbnd  13589  facwordi  13645  fi1uzind  13851  brfi1indALT  13854  unbenlem  16233  fiinopn  21504  cmpsublem  22002  dvcnvrelem1  24618  axcontlem4  26759  axcont  26768  spansncol  29349  atcvat4i  30178  sumdmdlem  30199  nocvxminlem  33321  broutsideof2  33657  relowlpssretop  34742  cvrat4  36697  pm2.43cbi  41158
 Copyright terms: Public domain W3C validator