Theorem simp1rl 1255

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

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

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 1103

This theorem is referenced by:  f1imass  7252  smo11  8339  zsupss  12949  lsmcv  21231  lspsolvlem  21232  mat2pmatghm  22844  mat2pmatmul  22845  plyadd  26331  plymul  26332  coeeu  26339  aannenlem1  26446  logexprlim  27343  ax5seglem6  29189  ax5seg  29193  mdetpmtr1  34125  mdetpmtr2  34126  wsuclem  36181  btwnconn1lem2  36446  btwnconn1lem3  36447  btwnconn1lem4  36448  btwnconn1lem12  36456  lshpsmreu  39740  2llnmat  40155  lvolex3N  40169  lnjatN  40411  pclfinclN  40581  lhpat3  40677  cdlemd6  40834  cdlemfnid  41195  cdlemk19ylem  41561  dihlsscpre  41865  dih1dimb2  41872  dihglblem6  41971  pellex  43419  tfsconcatrn  43926  mullimc  46191  mullimcf  46198  limcperiod  46203  cncfshift  46447  cncfperiod  46452  nprmmul2  48133