Theorem simp1l2 1284

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp3  8134  mapxpen  9119  lsmcv  21231  pmatcollpw2  22892  ltslpss  28055  btwnconn1lem4  36448  linethru  36511  hlrelat3  40043  cvrval3  40044  cvrval4N  40045  2atlt  40070  atbtwnex  40079  1cvratlt  40105  atcvrlln2  40150  atcvrlln  40151  2llnmat  40155  lvolnlelpln  40216  lnjatN  40411  lncmp  40414  cdlemd9  40837  dihord5b  41890  dihmeetALTN  41958  mapdrvallem2  42276  itschlc0xyqsol  49399