Theorem simp1l2 1286

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

Assertion

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

Proof of Theorem simp1l2

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8204  mapxpen  9200  lsmcv  21470  pmatcollpw2  23151  ltslpss  28351  btwnconn1lem4  37070  linethru  37133  hlrelat3  40735  cvrval3  40736  cvrval4N  40737  2atlt  40762  atbtwnex  40771  1cvratlt  40797  atcvrlln2  40842  atcvrlln  40843  2llnmat  40847  lvolnlelpln  40908  lnjatN  41103  lncmp  41106  cdlemd9  41529  dihord5b  42582  dihmeetALTN  42650  mapdrvallem2  42968  itschlc0xyqsol  50210