Theorem simp1l2 1268

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

Assertion

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

Proof of Theorem simp1l2

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

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

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 1088

This theorem is referenced by:  poxp3  8129  mapxpen  9107  lsmcv  21051  pmatcollpw2  22665  sltlpss  27819  btwnconn1lem4  36078  linethru  36141  hlrelat3  39406  cvrval3  39407  cvrval4N  39408  2atlt  39433  atbtwnex  39442  1cvratlt  39468  atcvrlln2  39513  atcvrlln  39514  2llnmat  39518  lvolnlelpln  39579  lnjatN  39774  lncmp  39777  cdlemd9  40200  dihord5b  41253  dihmeetALTN  41321  mapdrvallem2  41639  itschlc0xyqsol  48756