Theorem simpl3l 1228

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 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1187	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  tfisi  7800  omopth2  8536  ltmul1a  12013  xaddass  13178  xlemul2a  13218  swrdsbslen  14564  swrdspsleq  14565  dvdsadd2b  16199  pockthg  16789  psgnunilem4  19293  efgred  19544  ptbasin  22965  basqtop  23099  xrsmopn  24212  nosupbnd1lem3  27095  nosupbnd1lem4  27096  noinfbnd1lem3  27110  noinfbnd1lem4  27111  noinfbnd1lem5  27112  axpasch  27953  axcontlem4  27979  elwwlks2ons3im  28962  br4  34417  btwnintr  34680  btwnexch3  34681  btwnouttr2  34683  cgrxfr  34716  lineext  34737  btwnconn1lem13  34760  btwnconn1lem14  34761  btwnconn3  34764  brsegle  34769  brsegle2  34770  segleantisym  34776  outsideofeu  34792  lineunray  34808  lineelsb2  34809  cvrcmp  37818  atcvrj2b  37968  3dimlem3  37997  3dimlem3OLDN  37998  3dim3  38005  ps-1  38013  lplnnle2at  38077  2llnm3N  38105  lvolnle3at  38118  4atlem0a  38129  4atlem3  38132  4atlem3a  38133  lnatexN  38315  paddasslem8  38363  paddasslem9  38364  paddasslem10  38365  paddasslem12  38367  paddasslem13  38368  lhp2lt  38537  lhpexle2lem  38545  lhpexle3  38548  lhpmcvr3  38561  lhpat3  38582  4atex  38612  trlval2  38699  ltrnideq  38711  ltrnatlw  38719  trlnle  38722  trlval4  38724  cdlemd4  38737  cdlemd5  38738  cdleme16  38821  cdleme21  38873  cdleme21k  38874  cdleme27cl  38902  cdleme27N  38905  cdleme29ex  38910  cdleme43fsv1snlem  38956  cdleme40m  39003  cdleme46f2g2  39029  cdleme46f2g1  39030  trlord  39105  cdlemg8  39167  cdlemg15a  39191  cdlemg16z  39195  cdlemg18a  39214  cdlemg24  39224  cdlemg38  39251  cdlemg40  39253  trlcone  39264  cdlemj2  39358  tendoid0  39361  tendoconid  39365  cdlemk34  39446  cdlemk38  39451  cdlemkid4  39470  cdlemk35s-id  39474  cdlemk39s-id  39476  cdlemk53  39493  tendospcanN  39559  cdlemm10N  39654  dihvalcqpre  39771  dihopelvalcpre  39784  dihord5b  39795  dihglblem5apreN  39827  dihmeetlem16N  39858  dihmeetlem17N  39859  dvh3dim3N  39985  qirropth  41289  mzpcong  41354  jm2.26  41384  aomclem6  41444  limcleqr  44005  fourierdlem42  44510  itsclc0b  46978