Theorem simpl3r 1230

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  tfisi  7801  offsplitfpar  8057  omopth2  8537  ltmul1a  12014  xmulasslem3  13216  xadddi2  13227  swrdsbslen  14565  swrdspsleq  14566  dvdsadd2b  16200  pockthg  16790  psgnunilem4  19294  efgred  19545  marrepeval  21950  submaeval  21969  mdetmul  22010  minmar1eval  22036  ptbasin  22966  basqtop  23100  xrsmopn  24213  nosupbnd1lem3  27096  nosupbnd1lem4  27097  nosupbnd1lem5  27098  noinfbnd1lem3  27111  noinfbnd1lem4  27112  noinfbnd1lem5  27113  axpasch  27954  axeuclid  27976  elwwlks2ons3im  28963  br4  34418  btwnouttr2  34684  trisegint  34690  cgrxfr  34717  lineext  34738  btwnconn1lem13  34761  btwnconn1lem14  34762  btwnconn3  34765  brsegle  34770  brsegle2  34771  segleantisym  34777  outsideofeu  34793  lineunray  34809  lineelsb2  34810  cvrcmp  37819  atcvrj2b  37969  3dimlem3  37998  3dimlem3OLDN  37999  3dim3  38006  ps-1  38014  ps-2  38015  lplnnle2at  38078  2llnm3N  38106  4atlem0a  38130  4atlem3  38133  4atlem3a  38134  lnatexN  38316  paddasslem8  38364  paddasslem9  38365  paddasslem10  38366  paddasslem12  38368  paddasslem13  38369  lhpexle2lem  38546  lhpexle3  38549  lhpat3  38583  4atex  38613  trlval2  38700  trlval4  38725  cdleme16  38822  cdleme21  38874  cdleme21k  38875  cdleme27cl  38903  cdleme27N  38906  cdleme43fsv1snlem  38957  cdleme48fvg  39037  cdlemg8  39168  cdlemg15a  39192  cdlemg16z  39196  cdlemg24  39225  cdlemg38  39252  cdlemg40  39254  trlcone  39265  cdlemj2  39359  tendoid0  39362  tendoconid  39366  cdlemk34  39447  cdlemk38  39452  cdlemkid4  39471  cdlemk53  39494  tendospcanN  39560  dihvalcqpre  39772  dihmeetlem15N  39858  qirropth  41290  mzpcong  41355  jm2.26  41385  aomclem6  41445  islptre  43962  limccog  43963  limcleqr  43987  fourierdlem42  44492  elaa2  44577  itsclc0b  46960