Theorem simp1rl 1234

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

Assertion

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

Proof of Theorem simp1rl

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1imass  7021  smo11  8000  zsupss  12336  lsmcv  19912  lspsolvlem  19913  mat2pmatghm  21337  mat2pmatmul  21338  plyadd  24806  plymul  24807  coeeu  24814  aannenlem1  24916  logexprlim  25800  ax5seglem6  26719  ax5seg  26723  mdetpmtr1  31088  mdetpmtr2  31089  wsuclem  33112  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem12  33559  lshpsmreu  36244  2llnmat  36659  lvolex3N  36673  lnjatN  36915  pclfinclN  37085  lhpat3  37181  cdlemd6  37338  cdlemfnid  37699  cdlemk19ylem  38065  dihlsscpre  38369  dih1dimb2  38376  dihglblem6  38475  pellex  39430  mullimc  41895  mullimcf  41902  limcperiod  41907  cncfshift  42155  cncfperiod  42160