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  412  a2and  844  3imp231  1114  rexlimdv  3151  sbcimdvOLD  3819  reusv1  5357  reusv2lem3  5360  reusv3  5365  sbcop1  5450  funopsn  7099  isofrlem  7290  oprabidw  7393  oprabid  7394  sorpsscmpl  7676  tfindsg  7802  frxp  8063  poxp  8065  poseq  8095  reldmtpos  8170  tfrlem9  8336  tfr3  8350  odi  8531  omass  8532  pssnn  9119  isinf  9211  isinfOLD  9212  pssnnOLD  9216  ordiso2  9458  ordtypelem7  9467  preleqg  9558  cantnf  9636  indcardi  9984  dfac2b  10073  cfslb2n  10211  infpssrlem4  10249  axdc4lem  10398  zorn2lem7  10445  fpwwe2lem7  10580  grudomon  10760  distrlem5pr  10970  ltexprlem1  10979  axpre-sup  11112  bndndx  12419  uzind2  12603  elfznelfzo  13684  ssnn0fi  13897  leexp1a  14087  swrdswrdlem  14599  swrdswrd  14600  swrdccat3blem  14634  reuccatpfxs1lem  14641  cncongr1  16550  prm23ge5  16694  unbenlem  16787  infpnlem1  16789  initoeu1  17904  termoeu1  17911  ring1ne0  20022  neindisj2  22490  cmpsub  22767  gausslemma2dlem1a  26729  nocvxminlem  27139  negsprop  27355  uhgr2edg  28198  upgrewlkle2  28596  upgrwlkdvdelem  28726  usgr2pth  28754  wwlksm1edg  28868  frgr3vlem1  29259  3vfriswmgrlem  29263  frgrwopreglem4a  29296  frgrwopreg  29309  shscli  30301  mdbr3  31281  mdbr4  31282  dmdbr3  31289  dmdbr4  31290  mdslmd1i  31313  chjatom  31341  mdsymlem4  31390  cdj3lem2b  31421  bnj517  33537  3jaodd  34326  dfon2lem6  34402  funray  34754  imp5p  34812  bj-cbvalim  35138  bj-cbvexim  35139  bj-fvimacnv0  35786  brabg2  36204  neificl  36241  grpomndo  36363  rngoueqz  36428  subsubelfzo0  45632  fzoopth  45633  2ffzoeq  45634  ztprmneprm  46497
  Copyright terms: Public domain W3C validator