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

Theorem simpl2l 1227
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 1187 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  soisores  7273  frrlem4  8221  omopth2  8532  ttrcltr  9657  fin23lem11  10258  dedekind  11323  xaddass  13174  swrdsbslen  14558  swrdspsleq  14559  ntrivcvgmul  15792  pockthg  16783  gsumsgrpccat  18655  efgred  19535  decpmatmullem  22136  decpmatmul  22137  unconn  22796  basqtop  23078  utop2nei  23618  ucncn  23653  cxple2  26068  cxple2a  26070  nogesgn1ores  27038  nolt02o  27059  nogt01o  27060  nosupbnd1lem1  27072  nosupbnd1lem3  27074  nosupbnd1lem4  27075  nosupbnd1lem5  27076  noinfbnd1lem1  27087  noinfbnd1lem3  27089  noinfbnd1lem4  27090  noinfbnd1lem5  27091  noetalem1  27105  cofcut1  27261  ax5seglem1  27919  ax5seglem2  27920  axpasch  27932  axcontlem4  27958  1pthon2v  29139  cvmlift2lem10  33963  br4  34387  cgrcomim  34620  btwnintr  34650  btwnouttr2  34653  btwndiff  34658  btwnconn1lem14  34731  btwnconn3  34734  segcon2  34736  brsegle  34739  brsegle2  34740  segleantisym  34746  seglelin  34747  outsideofeu  34762  eqlkr  37607  eqlkr2  37608  lkrlsp  37610  atbtwn  37955  athgt  37965  3dimlem3  37970  3dimlem3OLDN  37971  3dim3  37978  3atlem7  37998  4atlem0a  38102  4atlem3a  38106  4atlem11  38118  lneq2at  38287  lnatexN  38288  cdlemb  38303  paddasslem6  38334  llnexchb2  38378  lhp2lt  38510  lhpexle2lem  38518  lhpexle3  38521  lhpmcvr3  38534  lhpat3  38555  ltrnnidn  38683  ltrneq3  38717  cdleme17b  38796  cdleme25a  38862  cdleme25dN  38865  cdleme27cl  38875  cdlemefrs29bpre0  38905  cdlemefs32sn1aw  38923  cdleme32le  38956  cdleme46f2g2  39002  cdleme46f2g1  39003  cdleme50trn3  39062  trlord  39078  ltrniotavalbN  39093  cdlemg6  39132  cdlemg7N  39135  cdlemg11b  39151  cdlemg15a  39164  cdlemg15  39165  cdlemg39  39225  trlcone  39237  cdlemg42  39238  tendoconid  39338  tendotr  39339  cdlemk39u  39477  cdlemk19u  39479  cdleml5N  39489  cdlemm10N  39627  dihord11b  39731  dihord2pre  39734  dihvalcqpre  39744  dihopelvalcpre  39757  dihord6apre  39765  dihord4  39767  dihord5b  39768  dihglblem5apreN  39800  dihmeetlem13N  39828  dihmeetlem19N  39834  dih1dimatlem0  39837  qirropth  41274  mzpcong  41339  jm2.25lem1  41365  jm2.26  41369  idomsubgmo  41568  fourierdlem42  44476  fourierdlem97  44530  line2  46924  itscnhlinecirc02plem2  46955
  Copyright terms: Public domain W3C validator