Theorem simpl3l 1245

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl3l	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl3l

Step	Hyp	Ref	Expression
1		simpll 778	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1204	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  tfisi  7854  omopth2  8568  ltmul1a  12063  xaddass  13274  xlemul2a  13314  swrdsbslen  14702  swrdspsleq  14703  dvdsadd2b  16363  pockthg  16965  psgnunilem4  19566  efgred  19817  ptbasin  23713  basqtop  23847  xrsmopn  24949  nosupbnd1lem3  27850  nosupbnd1lem4  27851  noinfbnd1lem3  27865  noinfbnd1lem4  27866  noinfbnd1lem5  27867  precsexlem8  28383  bdayfinbndlem1  28636  axpasch  29257  axcontlem4  29283  elwwlks2ons3im  30269  mhmimasplusg  33323  br4  36216  btwnintr  36477  btwnexch3  36478  btwnouttr2  36480  cgrxfr  36513  lineext  36534  btwnconn1lem13  36557  btwnconn1lem14  36558  btwnconn3  36561  brsegle  36566  brsegle2  36567  segleantisym  36573  outsideofeu  36589  lineunray  36605  lineelsb2  36606  cvrcmp  40025  atcvrj2b  40174  3dimlem3  40203  3dimlem3OLDN  40204  3dim3  40211  ps-1  40219  lplnnle2at  40283  2llnm3N  40311  lvolnle3at  40324  4atlem0a  40335  4atlem3  40338  4atlem3a  40339  lnatexN  40521  paddasslem8  40569  paddasslem9  40570  paddasslem10  40571  paddasslem12  40573  paddasslem13  40574  lhp2lt  40743  lhpexle2lem  40751  lhpexle3  40754  lhpmcvr3  40767  lhpat3  40788  4atex  40818  trlval2  40905  ltrnideq  40917  ltrnatlw  40925  trlnle  40928  trlval4  40930  cdlemd4  40943  cdlemd5  40944  cdleme16  41027  cdleme21  41079  cdleme21k  41080  cdleme27cl  41108  cdleme27N  41111  cdleme29ex  41116  cdleme43fsv1snlem  41162  cdleme40m  41209  cdleme46f2g2  41235  cdleme46f2g1  41236  trlord  41311  cdlemg8  41373  cdlemg15a  41397  cdlemg16z  41401  cdlemg18a  41420  cdlemg24  41430  cdlemg38  41457  cdlemg40  41459  trlcone  41470  cdlemj2  41564  tendoid0  41567  tendoconid  41571  cdlemk34  41652  cdlemk38  41657  cdlemkid4  41676  cdlemk35s-id  41680  cdlemk39s-id  41682  cdlemk53  41699  tendospcanN  41765  cdlemm10N  41860  dihvalcqpre  41977  dihopelvalcpre  41990  dihord5b  42001  dihglblem5apreN  42033  dihmeetlem16N  42064  dihmeetlem17N  42065  dvh3dim3N  42191  qirropth  43605  mzpcong  43669  jm2.26  43699  aomclem6  43756  limcleqr  46328  fourierdlem42  46833  submodneaddmod  48061  itsclc0b  49519