Theorem simpl3l 1235

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  tfisi  7806  omopth2  8516  ltmul1a  12002  xaddass  13199  xlemul2a  13239  swrdsbslen  14625  swrdspsleq  14626  dvdsadd2b  16273  pockthg  16875  psgnunilem4  19470  efgred  19721  ptbasin  23567  basqtop  23701  xrsmopn  24803  nosupbnd1lem3  27699  nosupbnd1lem4  27700  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  precsexlem8  28231  bdayfinbndlem1  28484  axpasch  29035  axcontlem4  29061  elwwlks2ons3im  30047  mhmimasplusg  33124  br4  35987  btwnintr  36248  btwnexch3  36249  btwnouttr2  36251  cgrxfr  36284  lineext  36305  btwnconn1lem13  36328  btwnconn1lem14  36329  btwnconn3  36332  brsegle  36337  brsegle2  36338  segleantisym  36344  outsideofeu  36360  lineunray  36376  lineelsb2  36377  cvrcmp  39776  atcvrj2b  39925  3dimlem3  39954  3dimlem3OLDN  39955  3dim3  39962  ps-1  39970  lplnnle2at  40034  2llnm3N  40062  lvolnle3at  40075  4atlem0a  40086  4atlem3  40089  4atlem3a  40090  lnatexN  40272  paddasslem8  40320  paddasslem9  40321  paddasslem10  40322  paddasslem12  40324  paddasslem13  40325  lhp2lt  40494  lhpexle2lem  40502  lhpexle3  40505  lhpmcvr3  40518  lhpat3  40539  4atex  40569  trlval2  40656  ltrnideq  40668  ltrnatlw  40676  trlnle  40679  trlval4  40681  cdlemd4  40694  cdlemd5  40695  cdleme16  40778  cdleme21  40830  cdleme21k  40831  cdleme27cl  40859  cdleme27N  40862  cdleme29ex  40867  cdleme43fsv1snlem  40913  cdleme40m  40960  cdleme46f2g2  40986  cdleme46f2g1  40987  trlord  41062  cdlemg8  41124  cdlemg15a  41148  cdlemg16z  41152  cdlemg18a  41171  cdlemg24  41181  cdlemg38  41208  cdlemg40  41210  trlcone  41221  cdlemj2  41315  tendoid0  41318  tendoconid  41322  cdlemk34  41403  cdlemk38  41408  cdlemkid4  41427  cdlemk35s-id  41431  cdlemk39s-id  41433  cdlemk53  41450  tendospcanN  41516  cdlemm10N  41611  dihvalcqpre  41728  dihopelvalcpre  41741  dihord5b  41752  dihglblem5apreN  41784  dihmeetlem16N  41815  dihmeetlem17N  41816  dvh3dim3N  41942  qirropth  43354  mzpcong  43418  jm2.26  43448  aomclem6  43505  limcleqr  46088  fourierdlem42  46593  submodneaddmod  47821  itsclc0b  49264