Theorem simp1rl 1235

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 1130	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  f1imass  7000  smo11  7984  zsupss  12325  lsmcv  19906  lspsolvlem  19907  mat2pmatghm  21335  mat2pmatmul  21336  plyadd  24814  plymul  24815  coeeu  24822  aannenlem1  24924  logexprlim  25809  ax5seglem6  26728  ax5seg  26732  mdetpmtr1  31176  mdetpmtr2  31177  wsuclem  33225  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem12  33672  lshpsmreu  36405  2llnmat  36820  lvolex3N  36834  lnjatN  37076  pclfinclN  37246  lhpat3  37342  cdlemd6  37499  cdlemfnid  37860  cdlemk19ylem  38226  dihlsscpre  38530  dih1dimb2  38537  dihglblem6  38636  pellex  39776  mullimc  42258  mullimcf  42265  limcperiod  42270  cncfshift  42516  cncfperiod  42521