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  7828  oalimcl  8618  oeordsuc  8652  fisup2g  9539  fiinf2g  9571  zorn2lem7  10573  inar1  10846  rpnnen1lem5  13048  expnbnd  14283  facwordi  14340  fi1uzind  14558  brfi1indALT  14561  unbenlem  16957  fiinopn  22930  cmpsublem  23430  dvcnvrelem1  26078  nocvxminlem  27842  axcontlem4  29002  axcont  29011  spansncol  31602  atcvat4i  32431  sumdmdlem  32452  broutsideof2  36088  relowlpssretop  37332  cvrat4  39402  pm2.43cbi  44491
  Copyright terms: Public domain W3C validator