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 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  f1imass  7264  smo11  8352  zsupss  12962  lsmcv  21246  lspsolvlem  21247  mat2pmatghm  22868  mat2pmatmul  22869  plyadd  26355  plymul  26356  coeeu  26363  aannenlem1  26472  logexprlim  27370  ax5seglem6  29265  ax5seg  29269  mdetpmtr1  34194  mdetpmtr2  34195  wsuclem  36296  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem12  36571  lshpsmreu  39864  2llnmat  40279  lvolex3N  40293  lnjatN  40535  pclfinclN  40705  lhpat3  40801  cdlemd6  40958  cdlemfnid  41319  cdlemk19ylem  41685  dihlsscpre  41989  dih1dimb2  41996  dihglblem6  42095  pellex  43545  tfsconcatrn  44052  mullimc  46315  mullimcf  46322  limcperiod  46327  cncfshift  46571  cncfperiod  46576  nprmmul2  48260