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

Theorem com4l 78
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by 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 75 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 77 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4t  79  com4r  80  com14  82  com5l  86  3impd  1165  merco2  1491  ax12b  1655  onint  4586  tfrlem1  6391  oalimcl  6558  oeordsuc  6592  fisup2g  7217  zorn2lem7  8129  inar1  8397  rpnnen1lem5  10346  expnbnd  11230  facwordi  11302  unbenlem  12955  fiinopn  16647  cmpsublem  17126  dvcnvrelem1  19364  spansncol  22147  atcvat4i  22977  sumdmdlem  22998  nocvxminlem  24344  axcontlem4  24595  axcont  24604  broutsideof2  24745  dfps2  25289  grpodivfo  25374  osneisi  25531  intopcoaconb  25540  fisub  25554  cmptdst  25568  prdnei  25573  limptlimpr2lem2  25575  bwt2  25592  addcanrg  25667  negveud  25668  negveudr  25669  distmlva  25688  hdrmp  25706  fnctartar  25907  fnctartar2  25908  cmpmor  25975  clscnc  26010  lppotos  26144  pm2.43cbi  28280  cvrat4  29632
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator