Theorem com3l 87

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 85	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 85	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  90  impd  446  expdcom  454  3imp3i2an  1270  rexlimdv  3012  sbcimdv  3465  reusv1  4792  reusv2lem3  4797  reusv3  4802  sotri2  5444  funopsn  6319  isofrlem  6490  oprabid  6576  sorpsscmpl  6846  tfindsg  6952  frxp  7174  poxp  7176  reldmtpos  7247  tfrlem9  7368  tfr3  7382  oawordri  7517  odi  7546  omass  7547  undifixp  7830  isinf  8058  pssnn  8063  ordiso2  8303  ordtypelem7  8312  cantnf  8473  indcardi  8747  dfac2  8836  cfslb2n  8973  infpssrlem4  9011  axdc4lem  9160  zorn2lem7  9207  fpwwe2lem8  9338  grudomon  9518  distrlem5pr  9728  ltexprlem1  9737  axpre-sup  9869  bndndx  11168  uzind2  11346  difreicc  12175  elfznelfzo  12439  ssnn0fi  12646  leexp1a  12781  swrdswrdlem  13311  swrdswrd  13312  swrdccat3blem  13346  cncongr1  15219  prm23ge5  15358  unbenlem  15450  infpnlem1  15452  initoeu1  16484  termoeu1  16491  ring1ne0  18414  neindisj2  20737  cmpsub  21013  gausslemma2dlem1a  24890  usgrafisinds  25942  wlkdvspth  26138  usgrcyclnl2  26169  wwlknred  26251  wwlkm1edg  26263  wlklenvclwlk  26366  el2spthonot  26397  2spontn0vne  26414  hashnbgravdg  26440  frgra3vlem1  26527  3vfriswmgralem  26531  vdn0frgrav2  26550  frgrawopreglem4  26574  numclwwlkovf2ex  26613  shscli  27560  mdbr3  28540  mdbr4  28541  dmdbr3  28548  dmdbr4  28549  mdslmd1i  28572  chjatom  28600  mdsymlem4  28649  cdj3lem2b  28680  bnj517  30209  3jaodd  30850  dfon2lem6  30937  poseq  30994  nocvxminlem  31089  funray  31417  imp5p  31475  brabg2  32680  neificl  32719  grpomndo  32844  rngoueqz  32909  eel12131  37959  3imp231  38066  reuccatpfxs1lem  40296  subsubelfzo0  40359  fzoopth  40360  2ffzoeq  40361  uhgr2edg  40435  1wlklenvclwlk  40863  upgrwlkdvdelem  40942  usgr2pth  40970  wwlksm1edg  41078  wspn0  41131  frgr3vlem1  41443  3vfriswmgrlem  41447  frgrwopreglem4  41484  av-numclwwlkovf2ex  41517  ztprmneprm  41918