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  1303  merco2  1701  onint  7037  oalimcl  7685  oeordsuc  7719  fisup2g  8415  fiinf2g  8447  zorn2lem7  9362  inar1  9635  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  expnbnd  13033  facwordi  13116  fi1uzind  13317  brfi1indALT  13320  unbenlem  15659  fiinopn  20754  cmpsublem  21250  dvcnvrelem1  23825  axcontlem4  25892  axcont  25901  spansncol  28555  atcvat4i  29384  sumdmdlem  29405  nocvxminlem  32018  broutsideof2  32354  relowlpssretop  33342  cvrat4  35047  pm2.43cbi  39041
 Copyright terms: Public domain W3C validator