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  411  a2and  839  3imp231  1105  rexlimdv  3280  sbcimdv  3840  reusv1  5288  reusv2lem3  5291  reusv3  5296  sbcop1  5370  funopsn  6902  isofrlem  7082  oprabidw  7176  oprabid  7177  sorpsscmpl  7449  tfindsg  7564  frxp  7809  poxp  7811  reldmtpos  7889  tfrlem9  8010  tfr3  8024  odi  8194  omass  8195  isinf  8719  pssnn  8724  ordiso2  8967  ordtypelem7  8976  preleqg  9066  cantnf  9144  indcardi  9455  dfac2b  9544  cfslb2n  9678  infpssrlem4  9716  axdc4lem  9865  zorn2lem7  9912  fpwwe2lem8  10047  grudomon  10227  distrlem5pr  10437  ltexprlem1  10446  axpre-sup  10579  bndndx  11884  uzind2  12063  elfznelfzo  13130  ssnn0fi  13341  leexp1a  13527  swrdswrdlem  14054  swrdswrd  14055  swrdccat3blem  14089  reuccatpfxs1lem  14096  cncongr1  15999  prm23ge5  16140  unbenlem  16232  infpnlem1  16234  initoeu1  17259  termoeu1  17266  ring1ne0  19270  neindisj2  21659  cmpsub  21936  gausslemma2dlem1a  25868  uhgr2edg  26917  upgrewlkle2  27315  wlklenvclwlkOLD  27364  upgrwlkdvdelem  27444  usgr2pth  27472  wwlksm1edg  27586  frgr3vlem1  27979  3vfriswmgrlem  27983  frgrwopreglem4a  28016  frgrwopreg  28029  shscli  29021  mdbr3  30001  mdbr4  30002  dmdbr3  30009  dmdbr4  30010  mdslmd1i  30033  chjatom  30061  mdsymlem4  30110  cdj3lem2b  30141  bnj517  32056  3jaodd  32841  dfon2lem6  32930  poseq  32992  nocvxminlem  33144  funray  33498  imp5p  33556  bj-cbvalim  33875  bj-cbvexim  33876  bj-fvimacnv0  34456  brabg2  34872  neificl  34909  grpomndo  35034  rngoueqz  35099  subsubelfzo0  43403  fzoopth  43404  2ffzoeq  43405  ztprmneprm  44323
  Copyright terms: Public domain W3C validator