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  8080  mapxpen  9056  lsmcv  21079  pmatcollpw2  22694  sltlpss  27854  btwnconn1lem4  36130  linethru  36193  hlrelat3  39457  cvrval3  39458  cvrval4N  39459  2atlt  39484  atbtwnex  39493  1cvratlt  39519  atcvrlln2  39564  atcvrlln  39565  2llnmat  39569  lvolnlelpln  39630  lnjatN  39825  lncmp  39828  cdlemd9  40251  dihord5b  41304  dihmeetALTN  41372  mapdrvallem2  41690  itschlc0xyqsol  48805