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

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

Proof of Theorem simpl2l
StepHypRef Expression
1 simpll 807 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl2 1199 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  soisores  6732  omopth2  7825  fin23lem11  9323  dedekind  10384  xaddass  12264  swrdsbslen  13640  ntrivcvgmul  14825  pockthg  15804  gsmsymgreqlem2  18043  efgred  18353  decpmatmullem  20770  decpmatmul  20771  unconn  21426  basqtop  21708  utop2nei  22247  ucncn  22282  cxple2  24634  cxple2a  24636  ax5seglem1  25999  ax5seglem2  26000  axpasch  26012  axcontlem4  26038  1pthon2v  27297  cvmlift2lem10  31593  br4  31947  frrlem4  32081  nolt02o  32143  nosupbnd1lem1  32152  nosupbnd1lem3  32154  nosupbnd1lem4  32155  nosupbnd1lem5  32156  cgrcomim  32394  btwnintr  32424  btwnouttr2  32427  btwndiff  32432  btwnconn1lem14  32505  btwnconn3  32508  segcon2  32510  brsegle  32513  brsegle2  32514  segleantisym  32520  seglelin  32521  outsideofeu  32536  eqlkr  34881  eqlkr2  34882  lkrlsp  34884  atbtwn  35227  athgt  35237  3dimlem3  35242  3dimlem3OLDN  35243  3dim3  35250  3atlem7  35270  4atlem0a  35374  4atlem3a  35378  4atlem11  35390  lneq2at  35559  lnatexN  35560  cdlemb  35575  paddasslem6  35606  llnexchb2  35650  lhp2lt  35782  lhpexle2lem  35790  lhpexle3  35793  lhpmcvr3  35806  lhpat3  35827  ltrnnidn  35956  ltrneq3  35990  cdleme17b  36069  cdleme25a  36135  cdleme25dN  36138  cdleme27cl  36148  cdlemefrs29bpre0  36178  cdlemefs32sn1aw  36196  cdleme32le  36229  cdleme46f2g2  36275  cdleme46f2g1  36276  cdleme50trn3  36335  trlord  36351  ltrniotavalbN  36366  cdlemg6  36405  cdlemg7N  36408  cdlemg11b  36424  cdlemg15a  36437  cdlemg15  36438  cdlemg39  36498  trlcone  36510  cdlemg42  36511  tendoconid  36611  tendotr  36612  cdlemk39u  36750  cdlemk19u  36752  cdleml5N  36762  cdlemm10N  36901  dihord11b  37005  dihord2pre  37008  dihvalcqpre  37018  dihopelvalcpre  37031  dihord6apre  37039  dihord4  37041  dihord5b  37042  dihglblem5apreN  37074  dihmeetlem13N  37102  dihmeetlem19N  37108  dih1dimatlem0  37111  qirropth  37967  mzpcong  38033  jm2.25lem1  38059  jm2.26  38063  idomsubgmo  38270  fourierdlem42  40861  fourierdlem97  40915
  Copyright terms: Public domain W3C validator