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  1348  merco2  1734  onint  7822  oalimcl  8612  oeordsuc  8646  fisup2g  9533  fiinf2g  9565  zorn2lem7  10567  inar1  10840  rpnnen1lem5  13042  expnbnd  14277  facwordi  14334  fi1uzind  14552  brfi1indALT  14555  unbenlem  16950  fiinopn  22921  cmpsublem  23421  dvcnvrelem1  26068  nocvxminlem  27831  axcontlem4  28991  axcont  29000  spansncol  31591  atcvat4i  32420  sumdmdlem  32441  broutsideof2  36078  relowlpssretop  37278  cvrat4  39348  pm2.43cbi  44429
  Copyright terms: Public domain W3C validator