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  1340  merco2  1728  onint  7498  oalimcl  8176  oeordsuc  8210  fisup2g  8921  fiinf2g  8953  zorn2lem7  9913  inar1  10186  rpnnen1lem5  12370  expnbnd  13583  facwordi  13639  fi1uzind  13845  brfi1indALT  13848  unbenlem  16234  fiinopn  21439  cmpsublem  21937  dvcnvrelem1  24543  axcontlem4  26681  axcont  26690  spansncol  29273  atcvat4i  30102  sumdmdlem  30123  nocvxminlem  33145  broutsideof2  33481  relowlpssretop  34528  cvrat4  36461  pm2.43cbi  40732
  Copyright terms: Public domain W3C validator