Theorem simpl3r 1226

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

Assertion

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

Proof of Theorem simpl3r

Step	Hyp	Ref	Expression
1		simplr 768	. 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  offsplitfpar  7798  omopth2  8193  ltmul1a  11478  xmulasslem3  12667  xadddi2  12678  swrdsbslen  14017  swrdspsleq  14018  dvdsadd2b  15648  pockthg  16232  psgnunilem4  18617  efgred  18866  marrepeval  21168  submaeval  21187  mdetmul  21228  minmar1eval  21254  ptbasin  22182  basqtop  22316  xrsmopn  23417  axpasch  26735  axeuclid  26757  elwwlks2ons3im  27740  br4  33107  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  btwnouttr2  33596  trisegint  33602  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  ps-2  36774  lplnnle2at  36837  2llnm3N  36865  4atlem0a  36889  4atlem3  36892  4atlem3a  36893  lnatexN  37075  paddasslem8  37123  paddasslem9  37124  paddasslem10  37125  paddasslem12  37127  paddasslem13  37128  lhpexle2lem  37305  lhpexle3  37308  lhpat3  37342  4atex  37372  trlval2  37459  trlval4  37484  cdleme16  37581  cdleme21  37633  cdleme21k  37634  cdleme27cl  37662  cdleme27N  37665  cdleme43fsv1snlem  37716  cdleme48fvg  37796  cdlemg8  37927  cdlemg15a  37951  cdlemg16z  37955  cdlemg24  37984  cdlemg38  38011  cdlemg40  38013  trlcone  38024  cdlemj2  38118  tendoid0  38121  tendoconid  38125  cdlemk34  38206  cdlemk38  38211  cdlemkid4  38230  cdlemk53  38253  tendospcanN  38319  dihvalcqpre  38531  dihmeetlem15N  38617  qirropth  39849  mzpcong  39913  jm2.26  39943  aomclem6  40003  islptre  42261  limccog  42262  limcleqr  42286  fourierdlem42  42791  elaa2  42876  itsclc0b  45186