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

Theorem simplr3 1214
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simplr3 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3
StepHypRef Expression
1 simp3 1135 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antlr 726 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  soltmin  5963  frfi  8747  wemappo  8997  iccsplit  12863  ccatswrd  14021  pfxccat3  14087  modfsummods  15140  pcdvdstr  16202  vdwlem12  16318  cshwsidrepswmod0  16420  iscatd2  16944  oppccomfpropd  16989  initoeu2lem0  17265  resssetc  17344  resscatc  17357  yonedalem4c  17519  mod1ile  17707  mod2ile  17708  prdsmndd  17936  grprcan  18129  mulgnn0dir  18249  mulgdir  18251  mulgass  18256  mulgnn0di  18939  mulgdi  18940  dprd2da  19157  lmodprop2d  19689  lssintcl  19729  prdslmodd  19734  islmhm2  19803  islbs2  19919  islbs3  19920  dmatmul  21102  mdetmul  21228  restopnb  21780  iunconn  22033  1stcelcls  22066  blsscls2  23111  stdbdbl  23124  xrsblre  23416  icccmplem2  23428  itg1val2  24288  cvxcl  25570  colline  26443  tglowdim2ln  26445  f1otrg  26665  f1otrge  26666  ax5seglem4  26726  ax5seglem5  26727  axcontlem3  26760  axcontlem8  26765  axcontlem9  26766  eengtrkg  26780  frgr3v  28060  xrofsup  30518  submomnd  30761  ogrpaddltbi  30769  erdszelem8  32555  resconn  32603  cvmliftmolem2  32639  cvmlift2lem12  32671  conway  33374  broutsideof3  33697  outsideoftr  33700  outsidele  33703  ltltncvr  36716  atcvrj2b  36725  cvrat4  36736  cvrat42  36737  2at0mat0  36818  islpln2a  36841  paddasslem11  37123  pmod1i  37141  lhpm0atN  37322  lautcvr  37385  cdlemg4c  37905  tendoplass  38076  tendodi1  38077  tendodi2  38078  dgrsub2  40074  grumnud  40989  ssinc  41718  ssdec  41719  ioondisj2  42125  ioondisj1  42126  ply1mulgsumlem2  44790
  Copyright terms: Public domain W3C validator