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

Theorem simpl2l 1223
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 766 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl2 1183 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  soisores  7063  omopth2  8197  fin23lem11  9732  dedekind  10796  xaddass  12634  swrdsbslen  14021  swrdspsleq  14022  ntrivcvgmul  15254  pockthg  16236  gsumsgrpccat  18000  efgred  18870  decpmatmullem  21380  decpmatmul  21381  unconn  22038  basqtop  22320  utop2nei  22860  ucncn  22895  cxple2  25292  cxple2a  25294  ax5seglem1  26726  ax5seglem2  26727  axpasch  26739  axcontlem4  26765  1pthon2v  27942  cvmlift2lem10  32673  br4  33108  frrlem4  33240  nolt02o  33313  nosupbnd1lem1  33322  nosupbnd1lem3  33324  nosupbnd1lem4  33325  nosupbnd1lem5  33326  cgrcomim  33564  btwnintr  33594  btwnouttr2  33597  btwndiff  33602  btwnconn1lem14  33675  btwnconn3  33678  segcon2  33680  brsegle  33683  brsegle2  33684  segleantisym  33690  seglelin  33691  outsideofeu  33706  eqlkr  36394  eqlkr2  36395  lkrlsp  36397  atbtwn  36741  athgt  36751  3dimlem3  36756  3dimlem3OLDN  36757  3dim3  36764  3atlem7  36784  4atlem0a  36888  4atlem3a  36892  4atlem11  36904  lneq2at  37073  lnatexN  37074  cdlemb  37089  paddasslem6  37120  llnexchb2  37164  lhp2lt  37296  lhpexle2lem  37304  lhpexle3  37307  lhpmcvr3  37320  lhpat3  37341  ltrnnidn  37469  ltrneq3  37503  cdleme17b  37582  cdleme25a  37648  cdleme25dN  37651  cdleme27cl  37661  cdlemefrs29bpre0  37691  cdlemefs32sn1aw  37709  cdleme32le  37742  cdleme46f2g2  37788  cdleme46f2g1  37789  cdleme50trn3  37848  trlord  37864  ltrniotavalbN  37879  cdlemg6  37918  cdlemg7N  37921  cdlemg11b  37937  cdlemg15a  37950  cdlemg15  37951  cdlemg39  38011  trlcone  38023  cdlemg42  38024  tendoconid  38124  tendotr  38125  cdlemk39u  38263  cdlemk19u  38265  cdleml5N  38275  cdlemm10N  38413  dihord11b  38517  dihord2pre  38520  dihvalcqpre  38530  dihopelvalcpre  38543  dihord6apre  38551  dihord4  38553  dihord5b  38554  dihglblem5apreN  38586  dihmeetlem13N  38614  dihmeetlem19N  38620  dih1dimatlem0  38623  qirropth  39842  mzpcong  39906  jm2.25lem1  39932  jm2.26  39936  idomsubgmo  40135  fourierdlem42  42784  fourierdlem97  42838  line2  45159  itscnhlinecirc02plem2  45190
  Copyright terms: Public domain W3C validator