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 782	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1151	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ 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 401  df-3an 1105

This theorem is used by:  f1imass  7262  smo11  8347  zsupss  12965  lsmcv  21274  lspsolvlem  21275  mat2pmatghm  22896  mat2pmatmul  22897  plyadd  26383  plymul  26384  coeeu  26391  aannenlem1  26500  logexprlim  27398  ax5seglem6  29293  ax5seg  29297  mdetpmtr1  34222  mdetpmtr2  34223  wsuclem  36323  btwnconn1lem2  36588  btwnconn1lem3  36589  btwnconn1lem4  36590  btwnconn1lem12  36598  lshpsmreu  39911  2llnmat  40326  lvolex3N  40340  lnjatN  40582  pclfinclN  40752  lhpat3  40848  cdlemd6  41005  cdlemfnid  41366  cdlemk19ylem  41732  dihlsscpre  42036  dih1dimb2  42043  dihglblem6  42142  pellex  43590  tfsconcatrn  44097  mullimc  46360  mullimcf  46367  limcperiod  46372  cncfshift  46616  cncfperiod  46621  nprmmul2  48305