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

Theorem com3l 86
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 84 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com3r 84 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  89  impd  445  expdcom  453  3imp3i2an  1269  rexlimdv  3011  sbcimdv  3464  reusv1  4786  reusv2lem3  4791  reusv3  4796  sotri2  5430  isofrlem  6467  oprabid  6553  sorpsscmpl  6823  tfindsg  6929  frxp  7151  poxp  7153  reldmtpos  7224  tfrlem9  7345  tfr3  7359  oawordri  7494  odi  7523  omass  7524  undifixp  7807  isinf  8035  pssnn  8040  ordiso2  8280  ordtypelem7  8289  cantnf  8450  indcardi  8724  dfac2  8813  cfslb2n  8950  infpssrlem4  8988  axdc4lem  9137  zorn2lem7  9184  fpwwe2lem8  9315  grudomon  9495  distrlem5pr  9705  ltexprlem1  9714  axpre-sup  9846  bndndx  11140  uzind2  11304  difreicc  12133  elfznelfzo  12396  ssnn0fi  12603  leexp1a  12738  swrdswrdlem  13259  swrdswrd  13260  swrdccat3blem  13294  cncongr1  15167  prm23ge5  15306  unbenlem  15398  infpnlem1  15400  initoeu1  16432  termoeu1  16439  ring1ne0  18362  neindisj2  20684  cmpsub  20960  gausslemma2dlem1a  24834  usgrafisinds  25735  wlkdvspth  25931  usgrcyclnl2  25962  wwlknred  26044  wwlkm1edg  26056  wlklenvclwlk  26159  el2spthonot  26190  2spontn0vne  26207  hashnbgravdg  26233  frgra3vlem1  26320  3vfriswmgralem  26324  vdn0frgrav2  26343  frgrawopreglem4  26367  numclwwlkovf2ex  26406  shscli  27353  mdbr3  28333  mdbr4  28334  dmdbr3  28341  dmdbr4  28342  mdslmd1i  28365  chjatom  28393  mdsymlem4  28442  cdj3lem2b  28473  bnj517  30002  3jaodd  30643  dfon2lem6  30730  poseq  30787  nocvxminlem  30882  funray  31210  imp5p  31268  brabg2  32463  neificl  32502  grpomndo  32627  rngoueqz  32692  eel12131  37742  3imp231  37849  reuccatpfxs1lem  40080  funopsn  40123  subsubelfzo0  40165  fzoopth  40166  2ffzoeq  40167  uhgr2edg  40416  1wlklenvclwlk  40844  upgrwlkdvdelem  40923  usgr2pth  40951  wwlksm1edg  41059  wspn0  41112  frgr3vlem1  41424  3vfriswmgrlem  41428  frgrwopreglem4  41465  av-numclwwlkovf2ex  41498  ztprmneprm  41899
  Copyright terms: Public domain W3C validator