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  846  3imp231  1113  rexlimdv  3136  reusv1  5339  reusv2lem3  5342  reusv3  5347  sbcop1  5441  funopsnOLD  7102  isofrlem  7295  oprabidw  7398  oprabid  7399  sorpsscmpl  7688  tfindsg  7812  frxp  8076  poxp  8078  poseq  8108  reldmtpos  8184  tfrlem9  8324  tfr3  8338  odi  8514  omass  8515  pssnn  9103  isinf  9175  ordiso2  9430  ordtypelem7  9439  preleqg  9536  cantnf  9614  indcardi  9963  dfac2b  10053  cfslb2n  10190  infpssrlem4  10228  axdc4lem  10377  zorn2lem7  10424  fpwwe2lem7  10560  grudomon  10740  distrlem5pr  10950  ltexprlem1  10959  axpre-sup  11092  bndndx  12436  uzind2  12622  fzoopth  13717  elfznelfzo  13728  ssnn0fi  13947  leexp1a  14137  swrdswrdlem  14666  swrdswrd  14667  swrdccat3blem  14701  reuccatpfxs1lem  14708  cncongr1  16636  prm23ge5  16786  unbenlem  16879  infpnlem1  16881  initoeu1  17978  termoeu1  17985  ring1ne0  20280  neindisj2  23088  cmpsub  23365  gausslemma2dlem1a  27328  nocvxminlem  27746  negsprop  28027  uhgr2edg  29277  upgrewlkle2  29675  upgrwlkdvdelem  29804  usgr2pth  29832  cyclnumvtx  29868  wwlksm1edg  29949  frgr3vlem1  30343  3vfriswmgrlem  30347  frgrwopreglem4a  30380  frgrwopreg  30393  shscli  31388  mdbr3  32368  mdbr4  32369  dmdbr3  32376  dmdbr4  32377  mdslmd1i  32400  chjatom  32428  mdsymlem4  32477  cdj3lem2b  32508  bnj517  35027  3jaodd  35897  dfon2lem6  35968  funray  36322  imp5p  36493  regsfromregtco  36720  bj-fvimacnv0  37600  brabg2  38038  neificl  38074  grpomndo  38196  rngoueqz  38261  relpfrlem  45380  subsubelfzo0  47775  2ffzoeq  47776  ztprmneprm  48823