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  3152  reusv1  5396  reusv2lem3  5399  reusv3  5404  sbcop1  5492  funopsn  7167  isofrlem  7361  oprabidw  7463  oprabid  7464  sorpsscmpl  7755  tfindsg  7883  frxp  8152  poxp  8154  poseq  8184  reldmtpos  8260  tfrlem9  8426  tfr3  8440  odi  8618  omass  8619  pssnn  9209  isinf  9297  isinfOLD  9298  ordiso2  9556  ordtypelem7  9565  preleqg  9656  cantnf  9734  indcardi  10082  dfac2b  10172  cfslb2n  10309  infpssrlem4  10347  axdc4lem  10496  zorn2lem7  10543  fpwwe2lem7  10678  grudomon  10858  distrlem5pr  11068  ltexprlem1  11077  axpre-sup  11210  bndndx  12527  uzind2  12713  fzoopth  13802  elfznelfzo  13812  ssnn0fi  14027  leexp1a  14216  swrdswrdlem  14743  swrdswrd  14744  swrdccat3blem  14778  reuccatpfxs1lem  14785  cncongr1  16705  prm23ge5  16854  unbenlem  16947  infpnlem1  16949  initoeu1  18057  termoeu1  18064  ring1ne0  20297  neindisj2  23132  cmpsub  23409  gausslemma2dlem1a  27410  nocvxminlem  27823  negsprop  28068  uhgr2edg  29226  upgrewlkle2  29625  upgrwlkdvdelem  29757  usgr2pth  29785  cyclnumvtx  29821  wwlksm1edg  29902  frgr3vlem1  30293  3vfriswmgrlem  30297  frgrwopreglem4a  30330  frgrwopreg  30343  shscli  31337  mdbr3  32317  mdbr4  32318  dmdbr3  32325  dmdbr4  32326  mdslmd1i  32349  chjatom  32377  mdsymlem4  32426  cdj3lem2b  32457  bnj517  34900  3jaodd  35716  dfon2lem6  35790  funray  36142  imp5p  36313  bj-cbvalim  36647  bj-cbvexim  36648  bj-fvimacnv0  37288  brabg2  37725  neificl  37761  grpomndo  37883  rngoueqz  37948  relpfrlem  44979  subsubelfzo0  47343  2ffzoeq  47344  ztprmneprm  48268