Theorem com3l 89

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com3l	⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Proof of Theorem com3l

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 87	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4l  92  impd  410  a2and  845  3imp231  1112  rexlimdv  3140  reusv1  5372  reusv2lem3  5375  reusv3  5380  sbcop1  5468  funopsn  7143  isofrlem  7338  oprabidw  7441  oprabid  7442  sorpsscmpl  7733  tfindsg  7861  frxp  8130  poxp  8132  poseq  8162  reldmtpos  8238  tfrlem9  8404  tfr3  8418  odi  8596  omass  8597  pssnn  9187  isinf  9273  isinfOLD  9274  ordiso2  9534  ordtypelem7  9543  preleqg  9634  cantnf  9712  indcardi  10060  dfac2b  10150  cfslb2n  10287  infpssrlem4  10325  axdc4lem  10474  zorn2lem7  10521  fpwwe2lem7  10656  grudomon  10836  distrlem5pr  11046  ltexprlem1  11055  axpre-sup  11188  bndndx  12505  uzind2  12691  fzoopth  13783  elfznelfzo  13793  ssnn0fi  14008  leexp1a  14198  swrdswrdlem  14727  swrdswrd  14728  swrdccat3blem  14762  reuccatpfxs1lem  14769  cncongr1  16691  prm23ge5  16840  unbenlem  16933  infpnlem1  16935  initoeu1  18029  termoeu1  18036  ring1ne0  20264  neindisj2  23066  cmpsub  23343  gausslemma2dlem1a  27333  nocvxminlem  27746  negsprop  27998  uhgr2edg  29192  upgrewlkle2  29591  upgrwlkdvdelem  29723  usgr2pth  29751  cyclnumvtx  29787  wwlksm1edg  29868  frgr3vlem1  30259  3vfriswmgrlem  30263  frgrwopreglem4a  30296  frgrwopreg  30309  shscli  31303  mdbr3  32283  mdbr4  32284  dmdbr3  32291  dmdbr4  32292  mdslmd1i  32315  chjatom  32343  mdsymlem4  32392  cdj3lem2b  32423  bnj517  34921  3jaodd  35737  dfon2lem6  35811  funray  36163  imp5p  36334  bj-cbvalim  36668  bj-cbvexim  36669  bj-fvimacnv0  37309  brabg2  37746  neificl  37782  grpomndo  37904  rngoueqz  37969  relpfrlem  44953  subsubelfzo0  47335  2ffzoeq  47336  ztprmneprm  48302