Theorem simp1l1 1268

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp3  8100  mapxpen  9081  hash7g  14448  lsmcv  21139  ltslpss  27900  archiabl  33259  trisegint  36210  linethru  36335  hlrelat3  39858  cvrval3  39859  cvrval4N  39860  2atlt  39885  atbtwnex  39894  1cvratlt  39920  atcvrlln2  39965  atcvrlln  39966  2llnmat  39970  lplnexllnN  40010  lvolnlelpln  40031  lnjatN  40226  lncvrat  40228  lncmp  40229  cdlemd9  40652  dihord5b  41705  dihmeetALTN  41773  dih1dimatlem0  41774  mapdrvallem2  42091  grumnudlem  44712