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  446  expdcom  454  3imp231  1277  rexlimdv  3059  sbcimdv  3531  reusv1  4896  reusv2lem3  4901  reusv3  4906  funopsn  6453  isofrlem  6630  oprabid  6717  sorpsscmpl  6990  tfindsg  7102  frxp  7332  poxp  7334  reldmtpos  7405  tfrlem9  7526  tfr3  7540  odi  7704  omass  7705  isinf  8214  pssnn  8219  ordiso2  8461  ordtypelem7  8470  cantnf  8628  indcardi  8902  dfac2  8991  cfslb2n  9128  infpssrlem4  9166  axdc4lem  9315  zorn2lem7  9362  fpwwe2lem8  9497  grudomon  9677  distrlem5pr  9887  ltexprlem1  9896  axpre-sup  10028  bndndx  11329  uzind2  11508  difreicc  12342  elfznelfzo  12613  ssnn0fi  12824  leexp1a  12959  swrdswrdlem  13505  swrdswrd  13506  swrdccat3blem  13541  cncongr1  15428  prm23ge5  15567  unbenlem  15659  infpnlem1  15661  initoeu1  16708  termoeu1  16715  ring1ne0  18637  neindisj2  20975  cmpsub  21251  gausslemma2dlem1a  25135  uhgr2edg  26145  wlklenvclwlk  26607  upgrwlkdvdelem  26688  usgr2pth  26716  wwlksm1edg  26835  frgr3vlem1  27253  3vfriswmgrlem  27257  frgrwopreglem4a  27290  frgrwopreg  27303  shscli  28304  mdbr3  29284  mdbr4  29285  dmdbr3  29292  dmdbr4  29293  mdslmd1i  29316  chjatom  29344  mdsymlem4  29393  cdj3lem2b  29424  bnj517  31081  3jaodd  31721  dfon2lem6  31817  poseq  31878  nocvxminlem  32018  funray  32372  imp5p  32430  brabg2  33640  neificl  33679  grpomndo  33804  rngoueqz  33869  subsubelfzo0  41661  fzoopth  41662  2ffzoeq  41663  reuccatpfxs1lem  41758  ztprmneprm  42450
  Copyright terms: Public domain W3C validator