MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com4l Structured version   Unicode version

Theorem com4l 84
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  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com4l  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )

Proof of Theorem com4l
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com3l 81 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 83 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
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  85  com4r  86  com14  88  com5l  92  3impd  1208  merco2  1573  onint  6603  oalimcl  7201  oeordsuc  7235  fisup2g  7918  zorn2lem7  8873  inar1  9142  rpnnen1lem5  11213  expnbnd  12277  facwordi  12349  brfi1uzind  12516  unbenlem  14510  fiinopn  19577  cmpsublem  20066  dvcnvrelem1  22584  axcontlem4  24472  axcont  24481  spansncol  26684  atcvat4i  27514  sumdmdlem  27535  nocvxminlem  29690  broutsideof2  30000  pm2.43cbi  33675  cvrat4  35564
  Copyright terms: Public domain W3C validator