Theorem simp1l2 1274

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp3  8097  mapxpen  9078  lsmcv  21141  pmatcollpw2  22768  ltslpss  27925  btwnconn1lem4  36325  linethru  36388  hlrelat3  39911  cvrval3  39912  cvrval4N  39913  2atlt  39938  atbtwnex  39947  1cvratlt  39973  atcvrlln2  40018  atcvrlln  40019  2llnmat  40023  lvolnlelpln  40084  lnjatN  40279  lncmp  40282  cdlemd9  40705  dihord5b  41758  dihmeetALTN  41826  mapdrvallem2  42144  itschlc0xyqsol  49265