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  842  3imp231  1110  rexlimdv  3145  sbcimdvOLD  3844  reusv1  5385  reusv2lem3  5388  reusv3  5393  sbcop1  5478  funopsn  7138  isofrlem  7329  oprabidw  7432  oprabid  7433  sorpsscmpl  7717  tfindsg  7843  frxp  8106  poxp  8108  poseq  8138  reldmtpos  8214  tfrlem9  8380  tfr3  8394  odi  8574  omass  8575  pssnn  9164  isinf  9256  isinfOLD  9257  pssnnOLD  9261  ordiso2  9506  ordtypelem7  9515  preleqg  9606  cantnf  9684  indcardi  10032  dfac2b  10121  cfslb2n  10259  infpssrlem4  10297  axdc4lem  10446  zorn2lem7  10493  fpwwe2lem7  10628  grudomon  10808  distrlem5pr  11018  ltexprlem1  11027  axpre-sup  11160  bndndx  12468  uzind2  12652  elfznelfzo  13734  ssnn0fi  13947  leexp1a  14137  swrdswrdlem  14651  swrdswrd  14652  swrdccat3blem  14686  reuccatpfxs1lem  14693  cncongr1  16601  prm23ge5  16747  unbenlem  16840  infpnlem1  16842  initoeu1  17963  termoeu1  17970  ring1ne0  20188  neindisj2  22949  cmpsub  23226  gausslemma2dlem1a  27214  nocvxminlem  27626  negsprop  27863  uhgr2edg  28934  upgrewlkle2  29332  upgrwlkdvdelem  29462  usgr2pth  29490  wwlksm1edg  29604  frgr3vlem1  29995  3vfriswmgrlem  29999  frgrwopreglem4a  30032  frgrwopreg  30045  shscli  31039  mdbr3  32019  mdbr4  32020  dmdbr3  32027  dmdbr4  32028  mdslmd1i  32051  chjatom  32079  mdsymlem4  32128  cdj3lem2b  32159  bnj517  34385  3jaodd  35179  dfon2lem6  35255  funray  35607  imp5p  35686  bj-cbvalim  36012  bj-cbvexim  36013  bj-fvimacnv0  36657  brabg2  37075  neificl  37111  grpomndo  37233  rngoueqz  37298  subsubelfzo0  46519  fzoopth  46520  2ffzoeq  46521  ztprmneprm  47212