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  3133  reusv1  5355  reusv2lem3  5358  reusv3  5363  sbcop1  5451  funopsn  7123  isofrlem  7318  oprabidw  7421  oprabid  7422  sorpsscmpl  7713  tfindsg  7840  frxp  8108  poxp  8110  poseq  8140  reldmtpos  8216  tfrlem9  8356  tfr3  8370  odi  8546  omass  8547  pssnn  9138  isinf  9214  isinfOLD  9215  ordiso2  9475  ordtypelem7  9484  preleqg  9575  cantnf  9653  indcardi  10001  dfac2b  10091  cfslb2n  10228  infpssrlem4  10266  axdc4lem  10415  zorn2lem7  10462  fpwwe2lem7  10597  grudomon  10777  distrlem5pr  10987  ltexprlem1  10996  axpre-sup  11129  bndndx  12448  uzind2  12634  fzoopth  13730  elfznelfzo  13740  ssnn0fi  13957  leexp1a  14147  swrdswrdlem  14676  swrdswrd  14677  swrdccat3blem  14711  reuccatpfxs1lem  14718  cncongr1  16644  prm23ge5  16793  unbenlem  16886  infpnlem1  16888  initoeu1  17980  termoeu1  17987  ring1ne0  20215  neindisj2  23017  cmpsub  23294  gausslemma2dlem1a  27283  nocvxminlem  27696  negsprop  27948  uhgr2edg  29142  upgrewlkle2  29541  upgrwlkdvdelem  29673  usgr2pth  29701  cyclnumvtx  29737  wwlksm1edg  29818  frgr3vlem1  30209  3vfriswmgrlem  30213  frgrwopreglem4a  30246  frgrwopreg  30259  shscli  31253  mdbr3  32233  mdbr4  32234  dmdbr3  32241  dmdbr4  32242  mdslmd1i  32265  chjatom  32293  mdsymlem4  32342  cdj3lem2b  32373  bnj517  34882  3jaodd  35709  dfon2lem6  35783  funray  36135  imp5p  36306  bj-cbvalim  36640  bj-cbvexim  36641  bj-fvimacnv0  37281  brabg2  37718  neificl  37754  grpomndo  37876  rngoueqz  37941  relpfrlem  44950  subsubelfzo0  47331  2ffzoeq  47332  ztprmneprm  48339