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  3140  reusv1  5377  reusv2lem3  5380  reusv3  5385  sbcop1  5473  funopsn  7148  isofrlem  7342  oprabidw  7444  oprabid  7445  sorpsscmpl  7736  tfindsg  7864  frxp  8133  poxp  8135  poseq  8165  reldmtpos  8241  tfrlem9  8407  tfr3  8421  odi  8599  omass  8600  pssnn  9190  isinf  9278  isinfOLD  9279  ordiso2  9537  ordtypelem7  9546  preleqg  9637  cantnf  9715  indcardi  10063  dfac2b  10153  cfslb2n  10290  infpssrlem4  10328  axdc4lem  10477  zorn2lem7  10524  fpwwe2lem7  10659  grudomon  10839  distrlem5pr  11049  ltexprlem1  11058  axpre-sup  11191  bndndx  12508  uzind2  12694  fzoopth  13783  elfznelfzo  13793  ssnn0fi  14008  leexp1a  14197  swrdswrdlem  14724  swrdswrd  14725  swrdccat3blem  14759  reuccatpfxs1lem  14766  cncongr1  16686  prm23ge5  16835  unbenlem  16928  infpnlem1  16930  initoeu1  18027  termoeu1  18034  ring1ne0  20264  neindisj2  23077  cmpsub  23354  gausslemma2dlem1a  27345  nocvxminlem  27758  negsprop  28003  uhgr2edg  29153  upgrewlkle2  29552  upgrwlkdvdelem  29684  usgr2pth  29712  cyclnumvtx  29748  wwlksm1edg  29829  frgr3vlem1  30220  3vfriswmgrlem  30224  frgrwopreglem4a  30257  frgrwopreg  30270  shscli  31264  mdbr3  32244  mdbr4  32245  dmdbr3  32252  dmdbr4  32253  mdslmd1i  32276  chjatom  32304  mdsymlem4  32353  cdj3lem2b  32384  bnj517  34858  3jaodd  35674  dfon2lem6  35748  funray  36100  imp5p  36271  bj-cbvalim  36605  bj-cbvexim  36606  bj-fvimacnv0  37246  brabg2  37683  neificl  37719  grpomndo  37841  rngoueqz  37906  relpfrlem  44931  subsubelfzo0  47296  2ffzoeq  47297  ztprmneprm  48221