Theorem simpl3l 1229

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 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  7848  omopth2  8584  ltmul1a  12063  xaddass  13228  xlemul2a  13268  swrdsbslen  14614  swrdspsleq  14615  dvdsadd2b  16249  pockthg  16839  psgnunilem4  19365  efgred  19616  ptbasin  23081  basqtop  23215  xrsmopn  24328  nosupbnd1lem3  27213  nosupbnd1lem4  27214  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  precsexlem8  27663  axpasch  28230  axcontlem4  28256  elwwlks2ons3im  29239  br4  34759  btwnintr  35022  btwnexch3  35023  btwnouttr2  35025  cgrxfr  35058  lineext  35079  btwnconn1lem13  35102  btwnconn1lem14  35103  btwnconn3  35106  brsegle  35111  brsegle2  35112  segleantisym  35118  outsideofeu  35134  lineunray  35150  lineelsb2  35151  cvrcmp  38201  atcvrj2b  38351  3dimlem3  38380  3dimlem3OLDN  38381  3dim3  38388  ps-1  38396  lplnnle2at  38460  2llnm3N  38488  lvolnle3at  38501  4atlem0a  38512  4atlem3  38515  4atlem3a  38516  lnatexN  38698  paddasslem8  38746  paddasslem9  38747  paddasslem10  38748  paddasslem12  38750  paddasslem13  38751  lhp2lt  38920  lhpexle2lem  38928  lhpexle3  38931  lhpmcvr3  38944  lhpat3  38965  4atex  38995  trlval2  39082  ltrnideq  39094  ltrnatlw  39102  trlnle  39105  trlval4  39107  cdlemd4  39120  cdlemd5  39121  cdleme16  39204  cdleme21  39256  cdleme21k  39257  cdleme27cl  39285  cdleme27N  39288  cdleme29ex  39293  cdleme43fsv1snlem  39339  cdleme40m  39386  cdleme46f2g2  39412  cdleme46f2g1  39413  trlord  39488  cdlemg8  39550  cdlemg15a  39574  cdlemg16z  39578  cdlemg18a  39597  cdlemg24  39607  cdlemg38  39634  cdlemg40  39636  trlcone  39647  cdlemj2  39741  tendoid0  39744  tendoconid  39748  cdlemk34  39829  cdlemk38  39834  cdlemkid4  39853  cdlemk35s-id  39857  cdlemk39s-id  39859  cdlemk53  39876  tendospcanN  39942  cdlemm10N  40037  dihvalcqpre  40154  dihopelvalcpre  40167  dihord5b  40178  dihglblem5apreN  40210  dihmeetlem16N  40241  dihmeetlem17N  40242  dvh3dim3N  40368  qirropth  41694  mzpcong  41759  jm2.26  41789  aomclem6  41849  limcleqr  44408  fourierdlem42  44913  itsclc0b  47506