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 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

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

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 1089

This theorem is referenced by:  f1imass  7284  smo11  8404  zsupss  12979  lsmcv  21143  lspsolvlem  21144  mat2pmatghm  22736  mat2pmatmul  22737  plyadd  26256  plymul  26257  coeeu  26264  aannenlem1  26370  logexprlim  27269  ax5seglem6  28949  ax5seg  28953  mdetpmtr1  33822  mdetpmtr2  33823  wsuclem  35826  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem12  36099  lshpsmreu  39110  2llnmat  39526  lvolex3N  39540  lnjatN  39782  pclfinclN  39952  lhpat3  40048  cdlemd6  40205  cdlemfnid  40566  cdlemk19ylem  40932  dihlsscpre  41236  dih1dimb2  41243  dihglblem6  41342  pellex  42846  tfsconcatrn  43355  mullimc  45631  mullimcf  45638  limcperiod  45643  cncfshift  45889  cncfperiod  45894