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  3151  sbcimdvOLD  3866  reusv1  5403  reusv2lem3  5406  reusv3  5411  sbcop1  5499  funopsn  7168  isofrlem  7360  oprabidw  7462  oprabid  7463  sorpsscmpl  7753  tfindsg  7882  frxp  8150  poxp  8152  poseq  8182  reldmtpos  8258  tfrlem9  8424  tfr3  8438  odi  8616  omass  8617  pssnn  9207  isinf  9294  isinfOLD  9295  ordiso2  9553  ordtypelem7  9562  preleqg  9653  cantnf  9731  indcardi  10079  dfac2b  10169  cfslb2n  10306  infpssrlem4  10344  axdc4lem  10493  zorn2lem7  10540  fpwwe2lem7  10675  grudomon  10855  distrlem5pr  11065  ltexprlem1  11074  axpre-sup  11207  bndndx  12523  uzind2  12709  fzoopth  13798  elfznelfzo  13808  ssnn0fi  14023  leexp1a  14212  swrdswrdlem  14739  swrdswrd  14740  swrdccat3blem  14774  reuccatpfxs1lem  14781  cncongr1  16701  prm23ge5  16849  unbenlem  16942  infpnlem1  16944  initoeu1  18065  termoeu1  18072  ring1ne0  20313  neindisj2  23147  cmpsub  23424  gausslemma2dlem1a  27424  nocvxminlem  27837  negsprop  28082  uhgr2edg  29240  upgrewlkle2  29639  upgrwlkdvdelem  29769  usgr2pth  29797  wwlksm1edg  29911  frgr3vlem1  30302  3vfriswmgrlem  30306  frgrwopreglem4a  30339  frgrwopreg  30352  shscli  31346  mdbr3  32326  mdbr4  32327  dmdbr3  32334  dmdbr4  32335  mdslmd1i  32358  chjatom  32386  mdsymlem4  32435  cdj3lem2b  32466  bnj517  34878  3jaodd  35695  dfon2lem6  35770  funray  36122  imp5p  36294  bj-cbvalim  36628  bj-cbvexim  36629  bj-fvimacnv0  37269  brabg2  37704  neificl  37740  grpomndo  37862  rngoueqz  37927  subsubelfzo0  47276  2ffzoeq  47277  ztprmneprm  48192