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  411  a2and  840  3imp231  1106  rexlimdv  3248  sbcimdv  3777  reusv1  5196  reusv2lem3  5199  reusv3  5204  sbcop1  5278  funopsn  6780  isofrlem  6963  oprabid  7054  sorpsscmpl  7325  tfindsg  7438  frxp  7680  poxp  7682  reldmtpos  7758  tfrlem9  7880  tfr3  7894  odi  8062  omass  8063  isinf  8584  pssnn  8589  ordiso2  8832  ordtypelem7  8841  preleqg  8931  cantnf  9009  indcardi  9320  dfac2b  9409  cfslb2n  9543  infpssrlem4  9581  axdc4lem  9730  zorn2lem7  9777  fpwwe2lem8  9912  grudomon  10092  distrlem5pr  10302  ltexprlem1  10311  axpre-sup  10444  bndndx  11750  uzind2  11929  elfznelfzo  12996  ssnn0fi  13207  leexp1a  13393  swrdswrdlem  13906  swrdswrd  13907  swrdccat3blem  13941  reuccatpfxs1lem  13948  cncongr1  15844  prm23ge5  15985  unbenlem  16077  infpnlem1  16079  initoeu1  17104  termoeu1  17111  ring1ne0  19035  neindisj2  21419  cmpsub  21696  gausslemma2dlem1a  25627  uhgr2edg  26677  upgrewlkle2  27075  wlklenvclwlk  27123  upgrwlkdvdelem  27203  usgr2pth  27231  wwlksm1edg  27345  frgr3vlem1  27740  3vfriswmgrlem  27744  frgrwopreglem4a  27777  frgrwopreg  27790  shscli  28781  mdbr3  29761  mdbr4  29762  dmdbr3  29769  dmdbr4  29770  mdslmd1i  29793  chjatom  29821  mdsymlem4  29870  cdj3lem2b  29901  bnj517  31769  3jaodd  32554  dfon2lem6  32643  poseq  32706  nocvxminlem  32858  funray  33212  imp5p  33270  bj-cbvalim  33582  bj-cbvexim  33583  brabg2  34544  neificl  34581  grpomndo  34706  rngoueqz  34771  subsubelfzo0  43064  fzoopth  43065  2ffzoeq  43066  ztprmneprm  43895