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  8102  btwnconn1lem7  36309  btwnconn1lem12  36314  linethru  36369  hlrelat3  39788  cvrval3  39789  2atlt  39815  atbtwnex  39824  1cvratlt  39850  2llnmat  39900  lplnexllnN  39940  4atlem11  39985  lnjatN  40156  lncvrat  40158  lncmp  40159  cdlemd9  40582  dihord5b  41635  dihmeetALTN  41703  dih1dimatlem0  41704  mapdrvallem2  42021  grumnudlem  44641  itsclc0yqsol  49124  itschlc0xyqsol  49127