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  3137  reusv1  5334  reusv2lem3  5337  reusv3  5342  sbcop1  5436  funopsn  7095  isofrlem  7288  oprabidw  7391  oprabid  7392  sorpsscmpl  7681  tfindsg  7805  frxp  8069  poxp  8071  poseq  8101  reldmtpos  8177  tfrlem9  8317  tfr3  8331  odi  8507  omass  8508  pssnn  9096  isinf  9168  ordiso2  9423  ordtypelem7  9432  preleqg  9527  cantnf  9605  indcardi  9954  dfac2b  10044  cfslb2n  10181  infpssrlem4  10219  axdc4lem  10368  zorn2lem7  10415  fpwwe2lem7  10551  grudomon  10731  distrlem5pr  10941  ltexprlem1  10950  axpre-sup  11083  bndndx  12427  uzind2  12613  fzoopth  13708  elfznelfzo  13719  ssnn0fi  13938  leexp1a  14128  swrdswrdlem  14657  swrdswrd  14658  swrdccat3blem  14692  reuccatpfxs1lem  14699  cncongr1  16627  prm23ge5  16777  unbenlem  16870  infpnlem1  16872  initoeu1  17969  termoeu1  17976  ring1ne0  20271  neindisj2  23098  cmpsub  23375  gausslemma2dlem1a  27342  nocvxminlem  27760  negsprop  28041  uhgr2edg  29291  upgrewlkle2  29690  upgrwlkdvdelem  29819  usgr2pth  29847  cyclnumvtx  29883  wwlksm1edg  29964  frgr3vlem1  30358  3vfriswmgrlem  30362  frgrwopreglem4a  30395  frgrwopreg  30408  shscli  31403  mdbr3  32383  mdbr4  32384  dmdbr3  32391  dmdbr4  32392  mdslmd1i  32415  chjatom  32443  mdsymlem4  32492  cdj3lem2b  32523  bnj517  35043  3jaodd  35913  dfon2lem6  35984  funray  36338  imp5p  36509  regsfromregtco  36736  bj-fvimacnv0  37616  brabg2  38052  neificl  38088  grpomndo  38210  rngoueqz  38275  relpfrlem  45398  subsubelfzo0  47787  2ffzoeq  47788  ztprmneprm  48835