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  6887  oalimcl  7527  oeordsuc  7561  fisup2g  8257  fiinf2g  8289  zorn2lem7  9207  inar1  9476  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  expnbnd  12855  facwordi  12938  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  unbenlem  15450  fiinopn  20531  cmpsublem  21012  dvcnvrelem1  23584  axcontlem4  25647  axcont  25656  spansncol  27811  atcvat4i  28640  sumdmdlem  28661  nocvxminlem  31089  broutsideof2  31399  relowlpssretop  32388  cvrat4  33747  pm2.43cbi  37745
 Copyright terms: Public domain W3C validator