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  411  a2and  843  3imp231  1113  rexlimdv  3153  sbcimdvOLD  3851  reusv1  5394  reusv2lem3  5397  reusv3  5402  sbcop1  5487  funopsn  7142  isofrlem  7333  oprabidw  7436  oprabid  7437  sorpsscmpl  7720  tfindsg  7846  frxp  8108  poxp  8110  poseq  8140  reldmtpos  8215  tfrlem9  8381  tfr3  8395  odi  8575  omass  8576  pssnn  9164  isinf  9256  isinfOLD  9257  pssnnOLD  9261  ordiso2  9506  ordtypelem7  9515  preleqg  9606  cantnf  9684  indcardi  10032  dfac2b  10121  cfslb2n  10259  infpssrlem4  10297  axdc4lem  10446  zorn2lem7  10493  fpwwe2lem7  10628  grudomon  10808  distrlem5pr  11018  ltexprlem1  11027  axpre-sup  11160  bndndx  12467  uzind2  12651  elfznelfzo  13733  ssnn0fi  13946  leexp1a  14136  swrdswrdlem  14650  swrdswrd  14651  swrdccat3blem  14685  reuccatpfxs1lem  14692  cncongr1  16600  prm23ge5  16744  unbenlem  16837  infpnlem1  16839  initoeu1  17957  termoeu1  17964  ring1ne0  20104  neindisj2  22618  cmpsub  22895  gausslemma2dlem1a  26857  nocvxminlem  27268  negsprop  27498  uhgr2edg  28454  upgrewlkle2  28852  upgrwlkdvdelem  28982  usgr2pth  29010  wwlksm1edg  29124  frgr3vlem1  29515  3vfriswmgrlem  29519  frgrwopreglem4a  29552  frgrwopreg  29565  shscli  30557  mdbr3  31537  mdbr4  31538  dmdbr3  31545  dmdbr4  31546  mdslmd1i  31569  chjatom  31597  mdsymlem4  31646  cdj3lem2b  31677  bnj517  33884  3jaodd  34672  dfon2lem6  34748  funray  35100  imp5p  35184  bj-cbvalim  35510  bj-cbvexim  35511  bj-fvimacnv0  36155  brabg2  36573  neificl  36609  grpomndo  36731  rngoueqz  36796  subsubelfzo0  46020  fzoopth  46021  2ffzoeq  46022  ztprmneprm  46976