Theorem simpl12 1247

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

Assertion

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

Proof of Theorem simpl12

Step	Hyp	Ref	Expression
1		simpl2 1190	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl1 1183	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  pythagtriplem4  16788  pmatcollpw1lem1  22689  pmatcollpw1  22691  mp2pm2mplem2  22722  nolt02o  27641  nogt01o  27642  brbtwn2  28729  ax5seg  28762  3vfriswmgr  30101  br8  35350  ifscgr  35640  seglecgr12im  35706  lkrshp  38577  atlatle  38792  cvlcvr1  38811  atbtwn  38919  3dimlem3  38934  3dimlem3OLDN  38935  1cvratex  38946  llnmlplnN  39012  4atlem3  39069  4atlem3a  39070  4atlem11  39082  4atlem12  39085  cdlemb  39267  paddasslem4  39296  paddasslem10  39302  pmodlem1  39319  llnexchb2lem  39341  arglem1N  39663  cdlemd4  39674  cdlemd  39680  cdleme16  39758  cdleme20  39797  cdleme21k  39811  cdleme22cN  39815  cdleme27N  39842  cdleme28c  39845  cdleme29ex  39847  cdleme32fva  39910  cdleme40n  39941  cdlemg15a  40128  cdlemg15  40129  cdlemg16ALTN  40131  cdlemg16z  40132  cdlemg20  40158  cdlemg22  40160  cdlemg29  40178  cdlemg38  40188  cdlemk33N  40382  cdlemk56  40444  fourierdlem77  45571

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »