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

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

Proof of Theorem simpl3l
StepHypRef Expression
1 simp3l 1087 . 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  7005  omopth2  7609  ltmul1a  10816  xaddass  12022  xlemul2a  12062  swrdsbslen  13386  dvdsadd2b  14952  pockthg  15534  psgnunilem4  17838  efgred  18082  ptbasin  21290  basqtop  21424  xrsmopn  22523  axpasch  25721  axcontlem4  25747  br4  31356  btwnintr  31768  btwnexch3  31769  btwnouttr2  31771  cgrxfr  31804  lineext  31825  btwnconn1lem13  31848  btwnconn1lem14  31849  btwnconn3  31852  brsegle  31857  brsegle2  31858  segleantisym  31864  outsideofeu  31880  lineunray  31896  lineelsb2  31897  cvrcmp  34050  atcvrj2b  34198  3dimlem3  34227  3dimlem3OLDN  34228  3dim3  34235  ps-1  34243  lplnnle2at  34307  2llnm3N  34335  lvolnle3at  34348  4atlem0a  34359  4atlem3  34362  4atlem3a  34363  lnatexN  34545  paddasslem8  34593  paddasslem9  34594  paddasslem10  34595  paddasslem12  34597  paddasslem13  34598  lhp2lt  34767  lhpexle2lem  34775  lhpexle3  34778  lhpmcvr3  34791  lhpat3  34812  4atex  34842  trlval2  34930  ltrnideq  34942  ltrnatlw  34950  trlnle  34953  trlval4  34955  cdlemd4  34968  cdlemd5  34969  cdleme16  35052  cdleme21  35105  cdleme21k  35106  cdleme27cl  35134  cdleme27N  35137  cdleme29ex  35142  cdleme43fsv1snlem  35188  cdleme40m  35235  cdleme46f2g2  35261  cdleme46f2g1  35262  trlord  35337  cdlemg8  35399  cdlemg15a  35423  cdlemg16z  35427  cdlemg18a  35446  cdlemg24  35456  cdlemg38  35483  cdlemg40  35485  trlcone  35496  cdlemj2  35590  tendoid0  35593  tendoconid  35597  cdlemk34  35678  cdlemk38  35683  cdlemkid4  35702  cdlemk35s-id  35706  cdlemk39s-id  35708  cdlemk53  35725  tendospcanN  35792  cdlemm10N  35887  dihvalcqpre  36004  dihopelvalcpre  36017  dihord5b  36028  dihglblem5apreN  36060  dihmeetlem16N  36091  dihmeetlem17N  36092  dvh3dim3N  36218  qirropth  36953  mzpcong  37019  jm2.26  37049  aomclem6  37109  limcleqr  39280  fourierdlem42  39673
  Copyright terms: Public domain W3C validator