Theorem simpl3l 1227

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 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1186	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  7879  omopth2  8620  ltmul1a  12113  xaddass  13287  xlemul2a  13327  swrdsbslen  14698  swrdspsleq  14699  dvdsadd2b  16339  pockthg  16939  psgnunilem4  19529  efgred  19780  ptbasin  23600  basqtop  23734  xrsmopn  24847  nosupbnd1lem3  27769  nosupbnd1lem4  27770  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  precsexlem8  28252  axpasch  28970  axcontlem4  28996  elwwlks2ons3im  29983  mhmimasplusg  33025  br4  35737  btwnintr  36000  btwnexch3  36001  btwnouttr2  36003  cgrxfr  36036  lineext  36057  btwnconn1lem13  36080  btwnconn1lem14  36081  btwnconn3  36084  brsegle  36089  brsegle2  36090  segleantisym  36096  outsideofeu  36112  lineunray  36128  lineelsb2  36129  cvrcmp  39264  atcvrj2b  39414  3dimlem3  39443  3dimlem3OLDN  39444  3dim3  39451  ps-1  39459  lplnnle2at  39523  2llnm3N  39551  lvolnle3at  39564  4atlem0a  39575  4atlem3  39578  4atlem3a  39579  lnatexN  39761  paddasslem8  39809  paddasslem9  39810  paddasslem10  39811  paddasslem12  39813  paddasslem13  39814  lhp2lt  39983  lhpexle2lem  39991  lhpexle3  39994  lhpmcvr3  40007  lhpat3  40028  4atex  40058  trlval2  40145  ltrnideq  40157  ltrnatlw  40165  trlnle  40168  trlval4  40170  cdlemd4  40183  cdlemd5  40184  cdleme16  40267  cdleme21  40319  cdleme21k  40320  cdleme27cl  40348  cdleme27N  40351  cdleme29ex  40356  cdleme43fsv1snlem  40402  cdleme40m  40449  cdleme46f2g2  40475  cdleme46f2g1  40476  trlord  40551  cdlemg8  40613  cdlemg15a  40637  cdlemg16z  40641  cdlemg18a  40660  cdlemg24  40670  cdlemg38  40697  cdlemg40  40699  trlcone  40710  cdlemj2  40804  tendoid0  40807  tendoconid  40811  cdlemk34  40892  cdlemk38  40897  cdlemkid4  40916  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53  40939  tendospcanN  41005  cdlemm10N  41100  dihvalcqpre  41217  dihopelvalcpre  41230  dihord5b  41241  dihglblem5apreN  41273  dihmeetlem16N  41304  dihmeetlem17N  41305  dvh3dim3N  41431  qirropth  42895  mzpcong  42960  jm2.26  42990  aomclem6  43047  limcleqr  45599  fourierdlem42  46104  submodneaddmod  47290  itsclc0b  48621