Theorem simp1l3 1270

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

Assertion

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

Proof of Theorem simp1l3

Step	Hyp	Ref	Expression
1		simpl3 1195	. 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  btwnconn1lem7  36275  btwnconn1lem12  36280  linethru  36335  hlrelat3  39858  cvrval3  39859  2atlt  39885  atbtwnex  39894  1cvratlt  39920  2llnmat  39970  lplnexllnN  40010  4atlem11  40055  lnjatN  40226  lncvrat  40228  lncmp  40229  cdlemd9  40652  dihord5b  41705  dihmeetALTN  41773  dih1dimatlem0  41774  mapdrvallem2  42091  grumnudlem  44712  itsclc0yqsol  49240  itschlc0xyqsol  49243