Theorem simp1rl 1240

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

Assertion

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

Proof of Theorem simp1rl

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

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

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

This theorem is referenced by:  f1imass  7054  smo11  8079  zsupss  12498  lsmcv  20132  lspsolvlem  20133  mat2pmatghm  21581  mat2pmatmul  21582  plyadd  25065  plymul  25066  coeeu  25073  aannenlem1  25175  logexprlim  26060  ax5seglem6  26979  ax5seg  26983  mdetpmtr1  31441  mdetpmtr2  31442  wsuclem  33499  btwnconn1lem2  34076  btwnconn1lem3  34077  btwnconn1lem4  34078  btwnconn1lem12  34086  lshpsmreu  36809  2llnmat  37224  lvolex3N  37238  lnjatN  37480  pclfinclN  37650  lhpat3  37746  cdlemd6  37903  cdlemfnid  38264  cdlemk19ylem  38630  dihlsscpre  38934  dih1dimb2  38941  dihglblem6  39040  pellex  40301  mullimc  42775  mullimcf  42782  limcperiod  42787  cncfshift  43033  cncfperiod  43038