MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com3l Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 87 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com3r 87 1 (𝜓 → (𝜒 → (𝜑𝜃)))
Colors of variables: wff setvar class
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  398  expdcomOLD  405  3imp231  1133  rexlimdv  3217  sbcimdv  3692  reusv1  5063  reusv2lem3  5066  reusv3  5071  funopsn  6634  isofrlem  6811  oprabid  6902  sorpsscmpl  7175  tfindsg  7287  frxp  7518  poxp  7520  reldmtpos  7592  tfrlem9  7714  tfr3  7728  odi  7893  omass  7894  isinf  8409  pssnn  8414  ordiso2  8656  ordtypelem7  8665  preleqg  8754  cantnf  8834  indcardi  9144  dfac2b  9233  dfac2OLD  9235  cfslb2n  9372  infpssrlem4  9410  axdc4lem  9559  zorn2lem7  9606  fpwwe2lem8  9741  grudomon  9921  distrlem5pr  10131  ltexprlem1  10140  axpre-sup  10272  bndndx  11554  uzind2  11732  difreicc  12523  elfznelfzo  12793  ssnn0fi  13004  leexp1a  13138  swrdswrdlem  13679  swrdswrd  13680  swrdccat3blem  13715  cncongr1  15595  prm23ge5  15733  unbenlem  15825  infpnlem1  15827  initoeu1  16861  termoeu1  16868  ring1ne0  18789  neindisj2  21137  cmpsub  21413  gausslemma2dlem1a  25300  uhgr2edg  26311  wlklenvclwlk  26775  upgrwlkdvdelem  26856  usgr2pth  26884  wwlksm1edg  27004  frgr3vlem1  27444  3vfriswmgrlem  27448  frgrwopreglem4a  27481  frgrwopreg  27494  shscli  28501  mdbr3  29481  mdbr4  29482  dmdbr3  29489  dmdbr4  29490  mdslmd1i  29513  chjatom  29541  mdsymlem4  29590  cdj3lem2b  29621  bnj517  31275  3jaodd  31914  dfon2lem6  32010  poseq  32071  nocvxminlem  32211  funray  32565  imp5p  32623  brabg2  33819  neificl  33857  grpomndo  33982  rngoueqz  34047  subsubelfzo0  41908  fzoopth  41909  2ffzoeq  41910  reuccatpfxs1lem  42005  ztprmneprm  42690
  Copyright terms: Public domain W3C validator