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  3131  reusv1  5335  reusv2lem3  5338  reusv3  5343  sbcop1  5428  funopsn  7081  isofrlem  7274  oprabidw  7377  oprabid  7378  sorpsscmpl  7667  tfindsg  7791  frxp  8056  poxp  8058  poseq  8088  reldmtpos  8164  tfrlem9  8304  tfr3  8318  odi  8494  omass  8495  pssnn  9078  isinf  9149  ordiso2  9401  ordtypelem7  9410  preleqg  9505  cantnf  9583  indcardi  9929  dfac2b  10019  cfslb2n  10156  infpssrlem4  10194  axdc4lem  10343  zorn2lem7  10390  fpwwe2lem7  10525  grudomon  10705  distrlem5pr  10915  ltexprlem1  10924  axpre-sup  11057  bndndx  12377  uzind2  12563  fzoopth  13659  elfznelfzo  13670  ssnn0fi  13889  leexp1a  14079  swrdswrdlem  14608  swrdswrd  14609  swrdccat3blem  14643  reuccatpfxs1lem  14650  cncongr1  16575  prm23ge5  16724  unbenlem  16817  infpnlem1  16819  initoeu1  17915  termoeu1  17922  ring1ne0  20215  neindisj2  23036  cmpsub  23313  gausslemma2dlem1a  27301  nocvxminlem  27715  negsprop  27975  uhgr2edg  29184  upgrewlkle2  29583  upgrwlkdvdelem  29712  usgr2pth  29740  cyclnumvtx  29776  wwlksm1edg  29857  frgr3vlem1  30248  3vfriswmgrlem  30252  frgrwopreglem4a  30285  frgrwopreg  30298  shscli  31292  mdbr3  32272  mdbr4  32273  dmdbr3  32280  dmdbr4  32281  mdslmd1i  32304  chjatom  32332  mdsymlem4  32381  cdj3lem2b  32412  bnj517  34892  3jaodd  35747  dfon2lem6  35821  funray  36173  imp5p  36344  bj-cbvalim  36678  bj-cbvexim  36679  bj-fvimacnv0  37319  brabg2  37756  neificl  37792  grpomndo  37914  rngoueqz  37979  relpfrlem  44985  subsubelfzo0  47356  2ffzoeq  47357  ztprmneprm  48377