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  8093  mapxpen  9074  lsmcv  21131  pmatcollpw2  22753  ltslpss  27914  btwnconn1lem4  36288  linethru  36351  hlrelat3  39872  cvrval3  39873  cvrval4N  39874  2atlt  39899  atbtwnex  39908  1cvratlt  39934  atcvrlln2  39979  atcvrlln  39980  2llnmat  39984  lvolnlelpln  40045  lnjatN  40240  lncmp  40243  cdlemd9  40666  dihord5b  41719  dihmeetALTN  41787  mapdrvallem2  42105  itschlc0xyqsol  49255