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  7239  smo11  8333  zsupss  12896  lsmcv  21051  lspsolvlem  21052  mat2pmatghm  22617  mat2pmatmul  22618  plyadd  26122  plymul  26123  coeeu  26130  aannenlem1  26236  logexprlim  27136  ax5seglem6  28861  ax5seg  28865  mdetpmtr1  33813  mdetpmtr2  33814  wsuclem  35813  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem12  36086  lshpsmreu  39102  2llnmat  39518  lvolex3N  39532  lnjatN  39774  pclfinclN  39944  lhpat3  40040  cdlemd6  40197  cdlemfnid  40558  cdlemk19ylem  40924  dihlsscpre  41228  dih1dimb2  41235  dihglblem6  41334  pellex  42823  tfsconcatrn  43331  mullimc  45614  mullimcf  45621  limcperiod  45626  cncfshift  45872  cncfperiod  45877