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  3132  reusv1  5337  reusv2lem3  5340  reusv3  5345  sbcop1  5431  funopsn  7087  isofrlem  7280  oprabidw  7383  oprabid  7384  sorpsscmpl  7673  tfindsg  7797  frxp  8062  poxp  8064  poseq  8094  reldmtpos  8170  tfrlem9  8310  tfr3  8324  odi  8500  omass  8501  pssnn  9085  isinf  9156  ordiso2  9408  ordtypelem7  9417  preleqg  9512  cantnf  9590  indcardi  9939  dfac2b  10029  cfslb2n  10166  infpssrlem4  10204  axdc4lem  10353  zorn2lem7  10400  fpwwe2lem7  10535  grudomon  10715  distrlem5pr  10925  ltexprlem1  10934  axpre-sup  11067  bndndx  12387  uzind2  12572  fzoopth  13664  elfznelfzo  13675  ssnn0fi  13894  leexp1a  14084  swrdswrdlem  14613  swrdswrd  14614  swrdccat3blem  14648  reuccatpfxs1lem  14655  cncongr1  16580  prm23ge5  16729  unbenlem  16822  infpnlem1  16824  initoeu1  17920  termoeu1  17927  ring1ne0  20219  neindisj2  23039  cmpsub  23316  gausslemma2dlem1a  27304  nocvxminlem  27718  negsprop  27978  uhgr2edg  29188  upgrewlkle2  29587  upgrwlkdvdelem  29716  usgr2pth  29744  cyclnumvtx  29780  wwlksm1edg  29861  frgr3vlem1  30255  3vfriswmgrlem  30259  frgrwopreglem4a  30292  frgrwopreg  30305  shscli  31299  mdbr3  32279  mdbr4  32280  dmdbr3  32287  dmdbr4  32288  mdslmd1i  32311  chjatom  32339  mdsymlem4  32388  cdj3lem2b  32419  bnj517  34918  3jaodd  35780  dfon2lem6  35851  funray  36205  imp5p  36376  bj-cbvalim  36710  bj-cbvexim  36711  bj-fvimacnv0  37351  brabg2  37777  neificl  37813  grpomndo  37935  rngoueqz  38000  relpfrlem  45070  subsubelfzo0  47450  2ffzoeq  47451  ztprmneprm  48471