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

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

Proof of Theorem simpl3r
StepHypRef Expression
1 simp3r 1083 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
21adantr 480 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  tfisi  6950  omopth2  7551  ltmul1a  10751  xmulasslem3  11988  xadddi2  11999  swrdsbslen  13300  swrdspsleq  13301  dvdsadd2b  14866  pockthg  15448  psgnunilem4  17740  efgred  17984  marrepeval  20188  submaeval  20207  mdetmul  20248  minmar1eval  20274  ptbasin  21190  basqtop  21324  xrsmopn  22423  axpasch  25621  axeuclid  25643  extwwlkfablem2  26605  br4  30901  btwnouttr2  31299  trisegint  31305  cgrxfr  31332  lineext  31353  btwnconn1lem13  31376  btwnconn1lem14  31377  btwnconn3  31380  brsegle  31385  brsegle2  31386  segleantisym  31392  outsideofeu  31408  lineunray  31424  lineelsb2  31425  cvrcmp  33588  atcvrj2b  33736  3dimlem3  33765  3dimlem3OLDN  33766  3dim3  33773  ps-1  33781  ps-2  33782  lplnnle2at  33845  2llnm3N  33873  4atlem0a  33897  4atlem3  33900  4atlem3a  33901  lnatexN  34083  paddasslem8  34131  paddasslem9  34132  paddasslem10  34133  paddasslem12  34135  paddasslem13  34136  lhpexle2lem  34313  lhpexle3  34316  lhpat3  34350  4atex  34380  trlval2  34468  trlval4  34493  cdleme16  34590  cdleme21  34643  cdleme21k  34644  cdleme27cl  34672  cdleme27N  34675  cdleme43fsv1snlem  34726  cdleme48fvg  34806  cdlemg8  34937  cdlemg15a  34961  cdlemg16z  34965  cdlemg24  34994  cdlemg38  35021  cdlemg40  35023  trlcone  35034  cdlemj2  35128  tendoid0  35131  tendoconid  35135  cdlemk34  35216  cdlemk38  35221  cdlemkid4  35240  cdlemk53  35263  tendospcanN  35330  dihvalcqpre  35542  dihmeetlem15N  35628  qirropth  36491  mzpcong  36557  jm2.26  36587  aomclem6  36647  islptre  38686  limccog  38687  limcleqr  38711  fourierdlem42  39042  elaa2  39127
  Copyright terms: Public domain W3C validator