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  7242  smo11  8336  zsupss  12903  lsmcv  21058  lspsolvlem  21059  mat2pmatghm  22624  mat2pmatmul  22625  plyadd  26129  plymul  26130  coeeu  26137  aannenlem1  26243  logexprlim  27143  ax5seglem6  28868  ax5seg  28872  mdetpmtr1  33820  mdetpmtr2  33821  wsuclem  35820  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem12  36093  lshpsmreu  39109  2llnmat  39525  lvolex3N  39539  lnjatN  39781  pclfinclN  39951  lhpat3  40047  cdlemd6  40204  cdlemfnid  40565  cdlemk19ylem  40931  dihlsscpre  41235  dih1dimb2  41242  dihglblem6  41341  pellex  42830  tfsconcatrn  43338  mullimc  45621  mullimcf  45628  limcperiod  45633  cncfshift  45879  cncfperiod  45884