Theorem simpl2l 1239

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

Step	Hyp	Ref	Expression
1		simpll 776	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl2 1199	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soisores  7307  frrlem4  8265  omopth2  8548  ttrcltr  9668  fin23lem11  10271  dedekind  11343  xaddass  13249  swrdsbslen  14675  swrdspsleq  14676  ntrivcvgmul  15915  pockthg  16925  gsumsgrpccat  18857  efgred  19771  decpmatmullem  22811  decpmatmul  22812  unconn  23469  basqtop  23751  utop2nei  24290  ucncn  24324  cxple2  26739  cxple2a  26741  nogesgn1ores  27715  nolt02o  27736  nogt01o  27737  nosupbnd1lem1  27749  nosupbnd1lem3  27751  nosupbnd1lem4  27752  nosupbnd1lem5  27753  noinfbnd1lem1  27764  noinfbnd1lem3  27766  noinfbnd1lem4  27767  noinfbnd1lem5  27768  noetalem1  27782  cofcut1  27990  bdayfinbndlem1  28537  ax5seglem1  29075  ax5seglem2  29076  axpasch  29088  axcontlem4  29114  1pthon2v  30301  mhmimasplusg  33177  cvmlift2lem10  35626  br4  36072  cgrcomim  36303  btwnintr  36333  btwnouttr2  36336  btwndiff  36341  btwnconn1lem14  36414  btwnconn3  36417  segcon2  36419  brsegle  36422  brsegle2  36423  segleantisym  36429  seglelin  36430  outsideofeu  36445  eqlkr  39687  eqlkr2  39688  lkrlsp  39690  atbtwn  40034  athgt  40044  3dimlem3  40049  3dimlem3OLDN  40050  3dim3  40057  3atlem7  40077  4atlem0a  40181  4atlem3a  40185  4atlem11  40197  lneq2at  40366  lnatexN  40367  cdlemb  40382  paddasslem6  40413  llnexchb2  40457  lhp2lt  40589  lhpexle2lem  40597  lhpexle3  40600  lhpmcvr3  40613  lhpat3  40634  ltrnnidn  40762  ltrneq3  40796  cdleme17b  40875  cdleme25a  40941  cdleme25dN  40944  cdleme27cl  40954  cdlemefrs29bpre0  40984  cdlemefs32sn1aw  41002  cdleme32le  41035  cdleme46f2g2  41081  cdleme46f2g1  41082  cdleme50trn3  41141  trlord  41157  ltrniotavalbN  41172  cdlemg6  41211  cdlemg7N  41214  cdlemg11b  41230  cdlemg15a  41243  cdlemg15  41244  cdlemg39  41304  trlcone  41316  cdlemg42  41317  tendoconid  41417  tendotr  41418  cdlemk39u  41556  cdlemk19u  41558  cdleml5N  41568  cdlemm10N  41706  dihord11b  41810  dihord2pre  41813  dihvalcqpre  41823  dihopelvalcpre  41836  dihord6apre  41844  dihord4  41846  dihord5b  41847  dihglblem5apreN  41879  dihmeetlem13N  41907  dihmeetlem19N  41913  dih1dimatlem0  41916  qirropth  43449  mzpcong  43513  jm2.25lem1  43539  jm2.26  43543  idomsubgmo  43734  fourierdlem42  46687  fourierdlem97  46741  clnbgrgrimlem  48519  line2  49338  itscnhlinecirc02plem2  49369