Theorem simpl2l 1222

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 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl2 1182	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  soisores  7082  omopth2  8212  fin23lem11  9741  dedekind  10805  xaddass  12645  swrdsbslen  14028  swrdspsleq  14029  ntrivcvgmul  15260  pockthg  16244  gsumsgrpccat  18006  efgred  18876  decpmatmullem  21381  decpmatmul  21382  unconn  22039  basqtop  22321  utop2nei  22861  ucncn  22896  cxple2  25282  cxple2a  25284  ax5seglem1  26716  ax5seglem2  26717  axpasch  26729  axcontlem4  26755  1pthon2v  27934  cvmlift2lem10  32561  br4  32996  frrlem4  33128  nolt02o  33201  nosupbnd1lem1  33210  nosupbnd1lem3  33212  nosupbnd1lem4  33213  nosupbnd1lem5  33214  cgrcomim  33452  btwnintr  33482  btwnouttr2  33485  btwndiff  33490  btwnconn1lem14  33563  btwnconn3  33566  segcon2  33568  brsegle  33571  brsegle2  33572  segleantisym  33578  seglelin  33579  outsideofeu  33594  eqlkr  36237  eqlkr2  36238  lkrlsp  36240  atbtwn  36584  athgt  36594  3dimlem3  36599  3dimlem3OLDN  36600  3dim3  36607  3atlem7  36627  4atlem0a  36731  4atlem3a  36735  4atlem11  36747  lneq2at  36916  lnatexN  36917  cdlemb  36932  paddasslem6  36963  llnexchb2  37007  lhp2lt  37139  lhpexle2lem  37147  lhpexle3  37150  lhpmcvr3  37163  lhpat3  37184  ltrnnidn  37312  ltrneq3  37346  cdleme17b  37425  cdleme25a  37491  cdleme25dN  37494  cdleme27cl  37504  cdlemefrs29bpre0  37534  cdlemefs32sn1aw  37552  cdleme32le  37585  cdleme46f2g2  37631  cdleme46f2g1  37632  cdleme50trn3  37691  trlord  37707  ltrniotavalbN  37722  cdlemg6  37761  cdlemg7N  37764  cdlemg11b  37780  cdlemg15a  37793  cdlemg15  37794  cdlemg39  37854  trlcone  37866  cdlemg42  37867  tendoconid  37967  tendotr  37968  cdlemk39u  38106  cdlemk19u  38108  cdleml5N  38118  cdlemm10N  38256  dihord11b  38360  dihord2pre  38363  dihvalcqpre  38373  dihopelvalcpre  38386  dihord6apre  38394  dihord4  38396  dihord5b  38397  dihglblem5apreN  38429  dihmeetlem13N  38457  dihmeetlem19N  38463  dih1dimatlem0  38466  qirropth  39512  mzpcong  39576  jm2.25lem1  39602  jm2.26  39606  idomsubgmo  39805  fourierdlem42  42441  fourierdlem97  42495  line2  44746  itscnhlinecirc02plem2  44777