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  3128  reusv1  5339  reusv2lem3  5342  reusv3  5347  sbcop1  5435  funopsn  7086  isofrlem  7281  oprabidw  7384  oprabid  7385  sorpsscmpl  7674  tfindsg  7801  frxp  8066  poxp  8068  poseq  8098  reldmtpos  8174  tfrlem9  8314  tfr3  8328  odi  8504  omass  8505  pssnn  9092  isinf  9165  isinfOLD  9166  ordiso2  9426  ordtypelem7  9435  preleqg  9530  cantnf  9608  indcardi  9954  dfac2b  10044  cfslb2n  10181  infpssrlem4  10219  axdc4lem  10368  zorn2lem7  10415  fpwwe2lem7  10550  grudomon  10730  distrlem5pr  10940  ltexprlem1  10949  axpre-sup  11082  bndndx  12401  uzind2  12587  fzoopth  13683  elfznelfzo  13693  ssnn0fi  13910  leexp1a  14100  swrdswrdlem  14628  swrdswrd  14629  swrdccat3blem  14663  reuccatpfxs1lem  14670  cncongr1  16596  prm23ge5  16745  unbenlem  16838  infpnlem1  16840  initoeu1  17936  termoeu1  17943  ring1ne0  20202  neindisj2  23026  cmpsub  23303  gausslemma2dlem1a  27292  nocvxminlem  27706  negsprop  27964  uhgr2edg  29171  upgrewlkle2  29570  upgrwlkdvdelem  29699  usgr2pth  29727  cyclnumvtx  29763  wwlksm1edg  29844  frgr3vlem1  30235  3vfriswmgrlem  30239  frgrwopreglem4a  30272  frgrwopreg  30285  shscli  31279  mdbr3  32259  mdbr4  32260  dmdbr3  32267  dmdbr4  32268  mdslmd1i  32291  chjatom  32319  mdsymlem4  32368  cdj3lem2b  32399  bnj517  34851  3jaodd  35687  dfon2lem6  35761  funray  36113  imp5p  36284  bj-cbvalim  36618  bj-cbvexim  36619  bj-fvimacnv0  37259  brabg2  37696  neificl  37732  grpomndo  37854  rngoueqz  37919  relpfrlem  44927  subsubelfzo0  47311  2ffzoeq  47312  ztprmneprm  48332