Theorem simp1rl 1257

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

Assertion

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

Proof of Theorem simp1rl

Step	Hyp	Ref	Expression
1		simprl 783	. 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:  f1imass  7269  smo11  8376  zsupss  13068  lsmcv  21425  lspsolvlem  21426  mat2pmatghm  23054  mat2pmatmul  23055  plyadd  26542  plymul  26543  coeeu  26550  aannenlem1  26661  logexprlim  27558  ax5seglem6  29518  ax5seg  29522  mdetpmtr1  34502  mdetpmtr2  34503  wsuclem  36680  btwnconn1lem2  36946  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem12  36956  lshpsmreu  40260  2llnmat  40675  lvolex3N  40689  lnjatN  40931  pclfinclN  41101  lhpat3  41197  cdlemd6  41354  cdlemfnid  41715  cdlemk19ylem  42081  dihlsscpre  42385  dih1dimb2  42392  dihglblem6  42491  pellex  43936  tfsconcatrn  44438  mullimc  46722  mullimcf  46729  limcperiod  46734  cncfshift  46978  cncfperiod  46983  nprmmul2  48704