Theorem simp1rl 1251

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

Assertion

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

Proof of Theorem simp1rl

Step	Hyp	Ref	Expression
1		simprl 780	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1145	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  f1imass  7242  smo11  8328  zsupss  12931  lsmcv  21198  lspsolvlem  21199  mat2pmatghm  22777  mat2pmatmul  22778  plyadd  26264  plymul  26265  coeeu  26272  aannenlem1  26379  logexprlim  27276  ax5seglem6  29091  ax5seg  29095  mdetpmtr1  34080  mdetpmtr2  34081  wsuclem  36133  btwnconn1lem2  36398  btwnconn1lem3  36399  btwnconn1lem4  36400  btwnconn1lem12  36408  lshpsmreu  39693  2llnmat  40108  lvolex3N  40122  lnjatN  40364  pclfinclN  40534  lhpat3  40630  cdlemd6  40787  cdlemfnid  41148  cdlemk19ylem  41514  dihlsscpre  41818  dih1dimb2  41825  dihglblem6  41924  pellex  43372  tfsconcatrn  43879  mullimc  46152  mullimcf  46159  limcperiod  46164  cncfshift  46408  cncfperiod  46413  nprmmul2  48094