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  413  a2and  841  3imp231  1109  rexlimdv  3283  sbcimdv  3842  reusv1  5297  reusv2lem3  5300  reusv3  5305  sbcop1  5378  funopsn  6909  isofrlem  7092  oprabidw  7186  oprabid  7187  sorpsscmpl  7459  tfindsg  7574  frxp  7819  poxp  7821  reldmtpos  7899  tfrlem9  8020  tfr3  8034  odi  8204  omass  8205  isinf  8730  pssnn  8735  ordiso2  8978  ordtypelem7  8987  preleqg  9077  cantnf  9155  indcardi  9466  dfac2b  9555  cfslb2n  9689  infpssrlem4  9727  axdc4lem  9876  zorn2lem7  9923  fpwwe2lem8  10058  grudomon  10238  distrlem5pr  10448  ltexprlem1  10457  axpre-sup  10590  bndndx  11895  uzind2  12074  elfznelfzo  13141  ssnn0fi  13352  leexp1a  13538  swrdswrdlem  14065  swrdswrd  14066  swrdccat3blem  14100  reuccatpfxs1lem  14107  cncongr1  16010  prm23ge5  16151  unbenlem  16243  infpnlem1  16245  initoeu1  17270  termoeu1  17277  ring1ne0  19340  neindisj2  21730  cmpsub  22007  gausslemma2dlem1a  25940  uhgr2edg  26989  upgrewlkle2  27387  wlklenvclwlkOLD  27436  upgrwlkdvdelem  27516  usgr2pth  27544  wwlksm1edg  27658  frgr3vlem1  28051  3vfriswmgrlem  28055  frgrwopreglem4a  28088  frgrwopreg  28101  shscli  29093  mdbr3  30073  mdbr4  30074  dmdbr3  30081  dmdbr4  30082  mdslmd1i  30105  chjatom  30133  mdsymlem4  30182  cdj3lem2b  30213  bnj517  32157  3jaodd  32944  dfon2lem6  33033  poseq  33095  nocvxminlem  33247  funray  33601  imp5p  33659  bj-cbvalim  33978  bj-cbvexim  33979  bj-fvimacnv0  34567  brabg2  34990  neificl  35027  grpomndo  35152  rngoueqz  35217  subsubelfzo0  43525  fzoopth  43526  2ffzoeq  43527  ztprmneprm  44394