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  8102  mapxpen  9083  lsmcv  21108  pmatcollpw2  22734  ltslpss  27916  btwnconn1lem4  36303  linethru  36366  hlrelat3  39785  cvrval3  39786  cvrval4N  39787  2atlt  39812  atbtwnex  39821  1cvratlt  39847  atcvrlln2  39892  atcvrlln  39893  2llnmat  39897  lvolnlelpln  39958  lnjatN  40153  lncmp  40156  cdlemd9  40579  dihord5b  41632  dihmeetALTN  41700  mapdrvallem2  42018  itschlc0xyqsol  49124