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  844  3imp231  1113  rexlimdv  3159  sbcimdvOLD  3879  reusv1  5415  reusv2lem3  5418  reusv3  5423  sbcop1  5508  funopsn  7182  isofrlem  7376  oprabidw  7479  oprabid  7480  sorpsscmpl  7769  tfindsg  7898  frxp  8167  poxp  8169  poseq  8199  reldmtpos  8275  tfrlem9  8441  tfr3  8455  odi  8635  omass  8636  pssnn  9234  isinf  9323  isinfOLD  9324  ordiso2  9584  ordtypelem7  9593  preleqg  9684  cantnf  9762  indcardi  10110  dfac2b  10200  cfslb2n  10337  infpssrlem4  10375  axdc4lem  10524  zorn2lem7  10571  fpwwe2lem7  10706  grudomon  10886  distrlem5pr  11096  ltexprlem1  11105  axpre-sup  11238  bndndx  12552  uzind2  12736  fzoopth  13812  elfznelfzo  13822  ssnn0fi  14036  leexp1a  14225  swrdswrdlem  14752  swrdswrd  14753  swrdccat3blem  14787  reuccatpfxs1lem  14794  cncongr1  16714  prm23ge5  16862  unbenlem  16955  infpnlem1  16957  initoeu1  18078  termoeu1  18085  ring1ne0  20322  neindisj2  23152  cmpsub  23429  gausslemma2dlem1a  27427  nocvxminlem  27840  negsprop  28085  uhgr2edg  29243  upgrewlkle2  29642  upgrwlkdvdelem  29772  usgr2pth  29800  wwlksm1edg  29914  frgr3vlem1  30305  3vfriswmgrlem  30309  frgrwopreglem4a  30342  frgrwopreg  30355  shscli  31349  mdbr3  32329  mdbr4  32330  dmdbr3  32337  dmdbr4  32338  mdslmd1i  32361  chjatom  32389  mdsymlem4  32438  cdj3lem2b  32469  bnj517  34861  3jaodd  35677  dfon2lem6  35752  funray  36104  imp5p  36277  bj-cbvalim  36611  bj-cbvexim  36612  bj-fvimacnv0  37252  brabg2  37677  neificl  37713  grpomndo  37835  rngoueqz  37900  subsubelfzo0  47241  2ffzoeq  47242  ztprmneprm  48072