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  841  3imp231  1111  rexlimdv  3211  sbcimdvOLD  3787  reusv1  5315  reusv2lem3  5318  reusv3  5323  sbcop1  5396  funopsn  7002  isofrlem  7191  oprabidw  7286  oprabid  7287  sorpsscmpl  7565  tfindsg  7682  frxp  7938  poxp  7940  reldmtpos  8021  tfrlem9  8187  tfr3  8201  odi  8372  omass  8373  pssnn  8913  isinf  8965  pssnnOLD  8969  ordiso2  9204  ordtypelem7  9213  preleqg  9303  cantnf  9381  indcardi  9728  dfac2b  9817  cfslb2n  9955  infpssrlem4  9993  axdc4lem  10142  zorn2lem7  10189  fpwwe2lem7  10324  grudomon  10504  distrlem5pr  10714  ltexprlem1  10723  axpre-sup  10856  bndndx  12162  uzind2  12343  elfznelfzo  13420  ssnn0fi  13633  leexp1a  13821  swrdswrdlem  14345  swrdswrd  14346  swrdccat3blem  14380  reuccatpfxs1lem  14387  cncongr1  16300  prm23ge5  16444  unbenlem  16537  infpnlem1  16539  initoeu1  17642  termoeu1  17649  ring1ne0  19745  neindisj2  22182  cmpsub  22459  gausslemma2dlem1a  26418  uhgr2edg  27478  upgrewlkle2  27876  wlklenvclwlkOLD  27925  upgrwlkdvdelem  28005  usgr2pth  28033  wwlksm1edg  28147  frgr3vlem1  28538  3vfriswmgrlem  28542  frgrwopreglem4a  28575  frgrwopreg  28588  shscli  29580  mdbr3  30560  mdbr4  30561  dmdbr3  30568  dmdbr4  30569  mdslmd1i  30592  chjatom  30620  mdsymlem4  30669  cdj3lem2b  30700  bnj517  32765  3jaodd  33559  dfon2lem6  33670  poseq  33729  nocvxminlem  33899  funray  34369  imp5p  34427  bj-cbvalim  34753  bj-cbvexim  34754  bj-fvimacnv0  35384  brabg2  35801  neificl  35838  grpomndo  35960  rngoueqz  36025  subsubelfzo0  44706  fzoopth  44707  2ffzoeq  44708  ztprmneprm  45571