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

Theorem simpl3r 1115
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl3r (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl3r
StepHypRef Expression
1 simp3r 1088 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
21adantr 481 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  tfisi  7012  omopth2  7616  ltmul1a  10823  xmulasslem3  12066  xadddi2  12077  swrdsbslen  13393  swrdspsleq  13394  dvdsadd2b  14959  pockthg  15541  psgnunilem4  17845  efgred  18089  marrepeval  20297  submaeval  20316  mdetmul  20357  minmar1eval  20383  ptbasin  21299  basqtop  21433  xrsmopn  22534  axpasch  25734  axeuclid  25756  br4  31383  btwnouttr2  31798  trisegint  31804  cgrxfr  31831  lineext  31852  btwnconn1lem13  31875  btwnconn1lem14  31876  btwnconn3  31879  brsegle  31884  brsegle2  31885  segleantisym  31891  outsideofeu  31907  lineunray  31923  lineelsb2  31924  cvrcmp  34077  atcvrj2b  34225  3dimlem3  34254  3dimlem3OLDN  34255  3dim3  34262  ps-1  34270  ps-2  34271  lplnnle2at  34334  2llnm3N  34362  4atlem0a  34386  4atlem3  34389  4atlem3a  34390  lnatexN  34572  paddasslem8  34620  paddasslem9  34621  paddasslem10  34622  paddasslem12  34624  paddasslem13  34625  lhpexle2lem  34802  lhpexle3  34805  lhpat3  34839  4atex  34869  trlval2  34957  trlval4  34982  cdleme16  35079  cdleme21  35132  cdleme21k  35133  cdleme27cl  35161  cdleme27N  35164  cdleme43fsv1snlem  35215  cdleme48fvg  35295  cdlemg8  35426  cdlemg15a  35450  cdlemg16z  35454  cdlemg24  35483  cdlemg38  35510  cdlemg40  35512  trlcone  35523  cdlemj2  35617  tendoid0  35620  tendoconid  35624  cdlemk34  35705  cdlemk38  35710  cdlemkid4  35729  cdlemk53  35752  tendospcanN  35819  dihvalcqpre  36031  dihmeetlem15N  36117  qirropth  36980  mzpcong  37046  jm2.26  37076  aomclem6  37136  islptre  39278  limccog  39279  limcleqr  39303  fourierdlem42  39694  elaa2  39779
  Copyright terms: Public domain W3C validator