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  7260  smo11  8356  zsupss  13045  lsmcv  21399  lspsolvlem  21400  mat2pmatghm  23028  mat2pmatmul  23029  plyadd  26516  plymul  26517  coeeu  26524  aannenlem1  26637  logexprlim  27534  ax5seglem6  29494  ax5seg  29498  mdetpmtr1  34437  mdetpmtr2  34438  wsuclem  36557  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem12  36833  lshpsmreu  40134  2llnmat  40549  lvolex3N  40563  lnjatN  40805  pclfinclN  40975  lhpat3  41071  cdlemd6  41228  cdlemfnid  41589  cdlemk19ylem  41955  dihlsscpre  42259  dih1dimb2  42266  dihglblem6  42365  pellex  43795  tfsconcatrn  44302  mullimc  46572  mullimcf  46579  limcperiod  46584  cncfshift  46828  cncfperiod  46833  nprmmul2  48554