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  8088  mapxpen  9065  lsmcv  21082  pmatcollpw2  22696  sltlpss  27856  btwnconn1lem4  36157  linethru  36220  hlrelat3  39534  cvrval3  39535  cvrval4N  39536  2atlt  39561  atbtwnex  39570  1cvratlt  39596  atcvrlln2  39641  atcvrlln  39642  2llnmat  39646  lvolnlelpln  39707  lnjatN  39902  lncmp  39905  cdlemd9  40328  dihord5b  41381  dihmeetALTN  41449  mapdrvallem2  41767  itschlc0xyqsol  48895