Theorem com3l 90

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 88	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 88	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  impd  416  a2and  859  3imp231  1130  rexlimdv  3165  reusv1  5363  reusv2lem3  5366  reusv3  5371  sbcop1  5462  funopsnOLD  7176  isofrlem  7371  oprabidw  7474  oprabid  7475  sorpsscmpl  7774  tfindsg  7896  frxp  8165  poxp  8167  poseq  8202  reldmtpos  8279  tfrlem9  8421  tfr3  8435  odi  8615  omass  8616  pssnn  9212  isinf  9284  ordiso2  9536  ordtypelem7  9545  preleqg  9643  cantnf  9721  indcardi  10147  dfac2b  10236  cfslb2n  10373  infpssrlem4  10411  axdc4lem  10560  zorn2lem7  10607  fpwwe2lem7  10749  grudomon  10929  distrlem5pr  11139  ltexprlem1  11148  axpre-sup  11281  bndndx  12632  uzind2  12819  fzoopth  13924  elfznelfzo  13935  ssnn0fi  14155  leexp1a  14345  swrdswrdlem  14881  swrdswrd  14882  swrdccat3blem  14916  reuccatpfxs1lem  14923  cncongr1  16871  prm23ge5  17022  unbenlem  17115  infpnlem1  17117  initoeu1  18215  termoeu1  18222  ring1ne0  20560  neindisj2  23471  cmpsub  23748  gausslemma2dlem1a  27722  nocvxminlem  28170  negsprop  28451  uhgr2edg  29819  upgrewlkle2  30217  upgrwlkdvdelem  30352  usgr2pth  30380  cyclnumvtx  30418  wwlksm1edg  30500  frgr3vlem1  30904  3vfriswmgrlem  30908  frgrwopreglem4a  30941  frgrwopreg  30954  shscli  31949  mdbr3  32929  mdbr4  32930  dmdbr3  32937  dmdbr4  32938  mdslmd1i  32961  chjatom  32989  mdsymlem4  33038  cdj3lem2b  33069  bnj517  35585  3jaodd  36658  dfon2lem6  36728  funray  37083  imp5p  37278  regsfromregtco  37504  bj-fvimacnv0  38399  brabg2  38843  neificl  38879  grpomndo  39001  rngoueqz  39066  relpfrlem  46138  subsubelfzo0  48602  2ffzoeq  48603  ztprmneprm  49664