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  3161  reusv1  5358  reusv2lem3  5361  reusv3  5366  sbcop1  5457  funopsnOLD  7152  isofrlem  7348  oprabidw  7451  oprabid  7452  sorpsscmpl  7750  tfindsg  7872  frxp  8140  poxp  8142  poseq  8177  reldmtpos  8254  tfrlem9  8396  tfr3  8410  odi  8590  omass  8591  pssnn  9187  isinf  9259  ordiso2  9512  ordtypelem7  9521  preleqg  9619  cantnf  9697  indcardi  10123  dfac2b  10212  cfslb2n  10349  infpssrlem4  10387  axdc4lem  10536  zorn2lem7  10583  fpwwe2lem7  10725  grudomon  10905  distrlem5pr  11115  ltexprlem1  11124  axpre-sup  11257  bndndx  12608  uzind2  12795  fzoopth  13900  elfznelfzo  13911  ssnn0fi  14131  leexp1a  14321  swrdswrdlem  14857  swrdswrd  14858  swrdccat3blem  14892  reuccatpfxs1lem  14899  cncongr1  16847  prm23ge5  16998  unbenlem  17091  infpnlem1  17093  initoeu1  18191  termoeu1  18198  ring1ne0  20535  neindisj2  23446  cmpsub  23723  gausslemma2dlem1a  27697  nocvxminlem  28145  negsprop  28426  uhgr2edg  29794  upgrewlkle2  30192  upgrwlkdvdelem  30327  usgr2pth  30355  cyclnumvtx  30393  wwlksm1edg  30475  frgr3vlem1  30879  3vfriswmgrlem  30883  frgrwopreglem4a  30916  frgrwopreg  30929  shscli  31924  mdbr3  32904  mdbr4  32905  dmdbr3  32912  dmdbr4  32913  mdslmd1i  32936  chjatom  32964  mdsymlem4  33013  cdj3lem2b  33044  bnj517  35561  3jaodd  36572  dfon2lem6  36642  funray  36997  imp5p  37192  regsfromregtco  37418  bj-fvimacnv0  38300  brabg2  38744  neificl  38780  grpomndo  38902  rngoueqz  38967  relpfrlem  46036  subsubelfzo0  48490  2ffzoeq  48491  ztprmneprm  49552