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  414  a2and  842  3imp231  1110  rexlimdv  3207  sbcimdv  3768  reusv1  5269  reusv2lem3  5272  reusv3  5277  sbcop1  5350  funopsn  6906  isofrlem  7092  oprabidw  7186  oprabid  7187  sorpsscmpl  7463  tfindsg  7579  frxp  7830  poxp  7832  reldmtpos  7915  tfrlem9  8036  tfr3  8050  odi  8220  omass  8221  pssnn  8743  isinf  8774  pssnnOLD  8779  ordiso2  9017  ordtypelem7  9026  preleqg  9116  cantnf  9194  indcardi  9506  dfac2b  9595  cfslb2n  9733  infpssrlem4  9771  axdc4lem  9920  zorn2lem7  9967  fpwwe2lem7  10102  grudomon  10282  distrlem5pr  10492  ltexprlem1  10501  axpre-sup  10634  bndndx  11938  uzind2  12119  elfznelfzo  13196  ssnn0fi  13407  leexp1a  13594  swrdswrdlem  14118  swrdswrd  14119  swrdccat3blem  14153  reuccatpfxs1lem  14160  cncongr1  16068  prm23ge5  16212  unbenlem  16304  infpnlem1  16306  initoeu1  17342  termoeu1  17349  ring1ne0  19417  neindisj2  21828  cmpsub  22105  gausslemma2dlem1a  26053  uhgr2edg  27102  upgrewlkle2  27500  wlklenvclwlkOLD  27549  upgrwlkdvdelem  27629  usgr2pth  27657  wwlksm1edg  27771  frgr3vlem1  28162  3vfriswmgrlem  28166  frgrwopreglem4a  28199  frgrwopreg  28212  shscli  29204  mdbr3  30184  mdbr4  30185  dmdbr3  30192  dmdbr4  30193  mdslmd1i  30216  chjatom  30244  mdsymlem4  30293  cdj3lem2b  30324  bnj517  32389  3jaodd  33179  dfon2lem6  33284  poseq  33361  nocvxminlem  33561  funray  34017  imp5p  34075  bj-cbvalim  34398  bj-cbvexim  34399  bj-fvimacnv0  35007  brabg2  35460  neificl  35497  grpomndo  35619  rngoueqz  35684  subsubelfzo0  44279  fzoopth  44280  2ffzoeq  44281  ztprmneprm  45144