Theorem simp1l2 1269

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

Assertion

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

Proof of Theorem simp1l2

Step	Hyp	Ref	Expression
1		simpl2 1194	. 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  lsmcv  21139  pmatcollpw2  22743  ltslpss  27900  btwnconn1lem4  36272  linethru  36335  hlrelat3  39858  cvrval3  39859  cvrval4N  39860  2atlt  39885  atbtwnex  39894  1cvratlt  39920  atcvrlln2  39965  atcvrlln  39966  2llnmat  39970  lvolnlelpln  40031  lnjatN  40226  lncmp  40229  cdlemd9  40652  dihord5b  41705  dihmeetALTN  41773  mapdrvallem2  42091  itschlc0xyqsol  49243