Theorem simp1rl 1239

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

Assertion

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

Proof of Theorem simp1rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1imass  7257  smo11  8378  zsupss  12953  lsmcv  21102  lspsolvlem  21103  mat2pmatghm  22668  mat2pmatmul  22669  plyadd  26174  plymul  26175  coeeu  26182  aannenlem1  26288  logexprlim  27188  ax5seglem6  28913  ax5seg  28917  mdetpmtr1  33854  mdetpmtr2  33855  wsuclem  35843  btwnconn1lem2  36106  btwnconn1lem3  36107  btwnconn1lem4  36108  btwnconn1lem12  36116  lshpsmreu  39127  2llnmat  39543  lvolex3N  39557  lnjatN  39799  pclfinclN  39969  lhpat3  40065  cdlemd6  40222  cdlemfnid  40583  cdlemk19ylem  40949  dihlsscpre  41253  dih1dimb2  41260  dihglblem6  41359  pellex  42858  tfsconcatrn  43366  mullimc  45645  mullimcf  45652  limcperiod  45657  cncfshift  45903  cncfperiod  45908