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  7198  smo11  8284  zsupss  12835  lsmcv  21079  lspsolvlem  21080  mat2pmatghm  22646  mat2pmatmul  22647  plyadd  26150  plymul  26151  coeeu  26158  aannenlem1  26264  logexprlim  27164  ax5seglem6  28913  ax5seg  28917  mdetpmtr1  33834  mdetpmtr2  33835  wsuclem  35865  btwnconn1lem2  36128  btwnconn1lem3  36129  btwnconn1lem4  36130  btwnconn1lem12  36138  lshpsmreu  39154  2llnmat  39569  lvolex3N  39583  lnjatN  39825  pclfinclN  39995  lhpat3  40091  cdlemd6  40248  cdlemfnid  40609  cdlemk19ylem  40975  dihlsscpre  41279  dih1dimb2  41286  dihglblem6  41385  pellex  42874  tfsconcatrn  43381  mullimc  45662  mullimcf  45669  limcperiod  45674  cncfshift  45918  cncfperiod  45923