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  5352  reusv2lem3  5355  reusv3  5360  sbcop1  5448  funopsn  7120  isofrlem  7315  oprabidw  7418  oprabid  7419  sorpsscmpl  7710  tfindsg  7837  frxp  8105  poxp  8107  poseq  8137  reldmtpos  8213  tfrlem9  8353  tfr3  8367  odi  8543  omass  8544  pssnn  9132  isinf  9207  isinfOLD  9208  ordiso2  9468  ordtypelem7  9477  preleqg  9568  cantnf  9646  indcardi  9994  dfac2b  10084  cfslb2n  10221  infpssrlem4  10259  axdc4lem  10408  zorn2lem7  10455  fpwwe2lem7  10590  grudomon  10770  distrlem5pr  10980  ltexprlem1  10989  axpre-sup  11122  bndndx  12441  uzind2  12627  fzoopth  13723  elfznelfzo  13733  ssnn0fi  13950  leexp1a  14140  swrdswrdlem  14669  swrdswrd  14670  swrdccat3blem  14704  reuccatpfxs1lem  14711  cncongr1  16637  prm23ge5  16786  unbenlem  16879  infpnlem1  16881  initoeu1  17973  termoeu1  17980  ring1ne0  20208  neindisj2  23010  cmpsub  23287  gausslemma2dlem1a  27276  nocvxminlem  27689  negsprop  27941  uhgr2edg  29135  upgrewlkle2  29534  upgrwlkdvdelem  29666  usgr2pth  29694  cyclnumvtx  29730  wwlksm1edg  29811  frgr3vlem1  30202  3vfriswmgrlem  30206  frgrwopreglem4a  30239  frgrwopreg  30252  shscli  31246  mdbr3  32226  mdbr4  32227  dmdbr3  32234  dmdbr4  32235  mdslmd1i  32258  chjatom  32286  mdsymlem4  32335  cdj3lem2b  32366  bnj517  34875  3jaodd  35702  dfon2lem6  35776  funray  36128  imp5p  36299  bj-cbvalim  36633  bj-cbvexim  36634  bj-fvimacnv0  37274  brabg2  37711  neificl  37747  grpomndo  37869  rngoueqz  37934  relpfrlem  44943  subsubelfzo0  47327  2ffzoeq  47328  ztprmneprm  48335