Theorem simpl3l 1229

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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1188	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfisi  7784  omopth2  8494  ltmul1a  11962  xaddass  13140  xlemul2a  13180  swrdsbslen  14564  swrdspsleq  14565  dvdsadd2b  16209  pockthg  16810  psgnunilem4  19402  efgred  19653  ptbasin  23485  basqtop  23619  xrsmopn  24721  nosupbnd1lem3  27642  nosupbnd1lem4  27643  noinfbnd1lem3  27657  noinfbnd1lem4  27658  noinfbnd1lem5  27659  precsexlem8  28145  axpasch  28912  axcontlem4  28938  elwwlks2ons3im  29925  mhmimasplusg  33009  br4  35770  btwnintr  36032  btwnexch3  36033  btwnouttr2  36035  cgrxfr  36068  lineext  36089  btwnconn1lem13  36112  btwnconn1lem14  36113  btwnconn3  36116  brsegle  36121  brsegle2  36122  segleantisym  36128  outsideofeu  36144  lineunray  36160  lineelsb2  36161  cvrcmp  39301  atcvrj2b  39450  3dimlem3  39479  3dimlem3OLDN  39480  3dim3  39487  ps-1  39495  lplnnle2at  39559  2llnm3N  39587  lvolnle3at  39600  4atlem0a  39611  4atlem3  39614  4atlem3a  39615  lnatexN  39797  paddasslem8  39845  paddasslem9  39846  paddasslem10  39847  paddasslem12  39849  paddasslem13  39850  lhp2lt  40019  lhpexle2lem  40027  lhpexle3  40030  lhpmcvr3  40043  lhpat3  40064  4atex  40094  trlval2  40181  ltrnideq  40193  ltrnatlw  40201  trlnle  40204  trlval4  40206  cdlemd4  40219  cdlemd5  40220  cdleme16  40303  cdleme21  40355  cdleme21k  40356  cdleme27cl  40384  cdleme27N  40387  cdleme29ex  40392  cdleme43fsv1snlem  40438  cdleme40m  40485  cdleme46f2g2  40511  cdleme46f2g1  40512  trlord  40587  cdlemg8  40649  cdlemg15a  40673  cdlemg16z  40677  cdlemg18a  40696  cdlemg24  40706  cdlemg38  40733  cdlemg40  40735  trlcone  40746  cdlemj2  40840  tendoid0  40843  tendoconid  40847  cdlemk34  40928  cdlemk38  40933  cdlemkid4  40952  cdlemk35s-id  40956  cdlemk39s-id  40958  cdlemk53  40975  tendospcanN  41041  cdlemm10N  41136  dihvalcqpre  41253  dihopelvalcpre  41266  dihord5b  41277  dihglblem5apreN  41309  dihmeetlem16N  41340  dihmeetlem17N  41341  dvh3dim3N  41467  qirropth  42920  mzpcong  42984  jm2.26  43014  aomclem6  43071  limcleqr  45661  fourierdlem42  46166  submodneaddmod  47361  itsclc0b  48783