Theorem simp1rl 1257

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

Assertion

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

Proof of Theorem simp1rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1imass  7265  smo11  8357  zsupss  12990  lsmcv  21334  lspsolvlem  21335  mat2pmatghm  22961  mat2pmatmul  22962  plyadd  26450  plymul  26451  coeeu  26458  aannenlem1  26571  logexprlim  27469  ax5seglem6  29399  ax5seg  29403  mdetpmtr1  34341  mdetpmtr2  34342  wsuclem  36410  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem12  36686  lshpsmreu  39990  2llnmat  40405  lvolex3N  40419  lnjatN  40661  pclfinclN  40831  lhpat3  40927  cdlemd6  41084  cdlemfnid  41445  cdlemk19ylem  41811  dihlsscpre  42115  dih1dimb2  42122  dihglblem6  42221  pellex  43684  tfsconcatrn  44191  mullimc  46454  mullimcf  46461  limcperiod  46466  cncfshift  46710  cncfperiod  46715  nprmmul2  48436