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

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

Proof of Theorem simpl3l
StepHypRef Expression
1 simp3l 1109 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
21adantr 480 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  tfisi  7100  omopth2  7709  ltmul1a  10910  xaddass  12117  xlemul2a  12157  swrdsbslen  13494  dvdsadd2b  15075  pockthg  15657  psgnunilem4  17963  efgred  18207  ptbasin  21428  basqtop  21562  xrsmopn  22662  axpasch  25866  axcontlem4  25892  elwwlks2ons3im  26919  br4  31774  nosupbnd1lem3  31981  nosupbnd1lem4  31982  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  cgrxfr  32287  lineext  32308  btwnconn1lem13  32331  btwnconn1lem14  32332  btwnconn3  32335  brsegle  32340  brsegle2  32341  segleantisym  32347  outsideofeu  32363  lineunray  32379  lineelsb2  32380  cvrcmp  34888  atcvrj2b  35036  3dimlem3  35065  3dimlem3OLDN  35066  3dim3  35073  ps-1  35081  lplnnle2at  35145  2llnm3N  35173  lvolnle3at  35186  4atlem0a  35197  4atlem3  35200  4atlem3a  35201  lnatexN  35383  paddasslem8  35431  paddasslem9  35432  paddasslem10  35433  paddasslem12  35435  paddasslem13  35436  lhp2lt  35605  lhpexle2lem  35613  lhpexle3  35616  lhpmcvr3  35629  lhpat3  35650  4atex  35680  trlval2  35768  ltrnideq  35780  ltrnatlw  35788  trlnle  35791  trlval4  35793  cdlemd4  35806  cdlemd5  35807  cdleme16  35890  cdleme21  35942  cdleme21k  35943  cdleme27cl  35971  cdleme27N  35974  cdleme29ex  35979  cdleme43fsv1snlem  36025  cdleme40m  36072  cdleme46f2g2  36098  cdleme46f2g1  36099  trlord  36174  cdlemg8  36236  cdlemg15a  36260  cdlemg16z  36264  cdlemg18a  36283  cdlemg24  36293  cdlemg38  36320  cdlemg40  36322  trlcone  36333  cdlemj2  36427  tendoid0  36430  tendoconid  36434  cdlemk34  36515  cdlemk38  36520  cdlemkid4  36539  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk53  36562  tendospcanN  36629  cdlemm10N  36724  dihvalcqpre  36841  dihopelvalcpre  36854  dihord5b  36865  dihglblem5apreN  36897  dihmeetlem16N  36928  dihmeetlem17N  36929  dvh3dim3N  37055  qirropth  37790  mzpcong  37856  jm2.26  37886  aomclem6  37946  limcleqr  40194  fourierdlem42  40684
  Copyright terms: Public domain W3C validator