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  3163  reusv1  5366  reusv2lem3  5369  reusv3  5374  sbcop1  5468  funopsnOLD  7149  isofrlem  7345  oprabidw  7448  oprabid  7449  sorpsscmpl  7739  tfindsg  7861  frxp  8128  poxp  8130  poseq  8160  reldmtpos  8236  tfrlem9  8378  tfr3  8392  odi  8570  omass  8571  pssnn  9167  isinf  9239  ordiso2  9491  ordtypelem7  9500  preleqg  9598  cantnf  9676  indcardi  10048  dfac2b  10137  cfslb2n  10274  infpssrlem4  10312  axdc4lem  10461  zorn2lem7  10508  fpwwe2lem7  10650  grudomon  10830  distrlem5pr  11040  ltexprlem1  11049  axpre-sup  11182  bndndx  12531  uzind2  12718  fzoopth  13822  elfznelfzo  13833  ssnn0fi  14053  leexp1a  14243  swrdswrdlem  14777  swrdswrd  14778  swrdccat3blem  14812  reuccatpfxs1lem  14819  cncongr1  16763  prm23ge5  16913  unbenlem  17006  infpnlem1  17008  initoeu1  18106  termoeu1  18113  ring1ne0  20447  neindisj2  23354  cmpsub  23631  gausslemma2dlem1a  27609  nocvxminlem  28027  negsprop  28308  uhgr2edg  29676  upgrewlkle2  30074  upgrwlkdvdelem  30209  usgr2pth  30237  cyclnumvtx  30275  wwlksm1edg  30357  frgr3vlem1  30761  3vfriswmgrlem  30765  frgrwopreglem4a  30798  frgrwopreg  30811  shscli  31806  mdbr3  32786  mdbr4  32787  dmdbr3  32794  dmdbr4  32795  mdslmd1i  32818  chjatom  32846  mdsymlem4  32895  cdj3lem2b  32926  bnj517  35402  3jaodd  36302  dfon2lem6  36373  funray  36728  imp5p  36939  regsfromregtco  37165  bj-fvimacnv0  38046  brabg2  38475  neificl  38511  grpomndo  38633  rngoueqz  38698  relpfrlem  45784  subsubelfzo0  48223  2ffzoeq  48224  ztprmneprm  49285