Theorem simpl3l 1225

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 1184	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  tfisi  7553  omopth2  8193  ltmul1a  11478  xaddass  12630  xlemul2a  12670  swrdsbslen  14017  swrdspsleq  14018  dvdsadd2b  15648  pockthg  16232  psgnunilem4  18617  efgred  18866  ptbasin  22182  basqtop  22316  xrsmopn  23417  axpasch  26735  axcontlem4  26761  elwwlks2ons3im  27740  br4  33107  nosupbnd1lem3  33323  nosupbnd1lem4  33324  btwnintr  33593  btwnexch3  33594  btwnouttr2  33596  cgrxfr  33629  lineext  33650  btwnconn1lem13  33673  btwnconn1lem14  33674  btwnconn3  33677  brsegle  33682  brsegle2  33683  segleantisym  33689  outsideofeu  33705  lineunray  33721  lineelsb2  33722  cvrcmp  36579  atcvrj2b  36728  3dimlem3  36757  3dimlem3OLDN  36758  3dim3  36765  ps-1  36773  lplnnle2at  36837  2llnm3N  36865  lvolnle3at  36878  4atlem0a  36889  4atlem3  36892  4atlem3a  36893  lnatexN  37075  paddasslem8  37123  paddasslem9  37124  paddasslem10  37125  paddasslem12  37127  paddasslem13  37128  lhp2lt  37297  lhpexle2lem  37305  lhpexle3  37308  lhpmcvr3  37321  lhpat3  37342  4atex  37372  trlval2  37459  ltrnideq  37471  ltrnatlw  37479  trlnle  37482  trlval4  37484  cdlemd4  37497  cdlemd5  37498  cdleme16  37581  cdleme21  37633  cdleme21k  37634  cdleme27cl  37662  cdleme27N  37665  cdleme29ex  37670  cdleme43fsv1snlem  37716  cdleme40m  37763  cdleme46f2g2  37789  cdleme46f2g1  37790  trlord  37865  cdlemg8  37927  cdlemg15a  37951  cdlemg16z  37955  cdlemg18a  37974  cdlemg24  37984  cdlemg38  38011  cdlemg40  38013  trlcone  38024  cdlemj2  38118  tendoid0  38121  tendoconid  38125  cdlemk34  38206  cdlemk38  38211  cdlemkid4  38230  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk53  38253  tendospcanN  38319  cdlemm10N  38414  dihvalcqpre  38531  dihopelvalcpre  38544  dihord5b  38555  dihglblem5apreN  38587  dihmeetlem16N  38618  dihmeetlem17N  38619  dvh3dim3N  38745  qirropth  39849  mzpcong  39913  jm2.26  39943  aomclem6  40003  limcleqr  42286  fourierdlem42  42791  itsclc0b  45186