Theorem simp1rl 1238

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  f1imass  7169  smo11  8226  zsupss  12723  lsmcv  20448  lspsolvlem  20449  mat2pmatghm  21924  mat2pmatmul  21925  plyadd  25423  plymul  25424  coeeu  25431  aannenlem1  25533  logexprlim  26418  ax5seglem6  27347  ax5seg  27351  mdetpmtr1  31818  mdetpmtr2  31819  wsuclem  33864  btwnconn1lem2  34435  btwnconn1lem3  34436  btwnconn1lem4  34437  btwnconn1lem12  34445  lshpsmreu  37165  2llnmat  37580  lvolex3N  37594  lnjatN  37836  pclfinclN  38006  lhpat3  38102  cdlemd6  38259  cdlemfnid  38620  cdlemk19ylem  38986  dihlsscpre  39290  dih1dimb2  39297  dihglblem6  39396  pellex  40694  mullimc  43206  mullimcf  43213  limcperiod  43218  cncfshift  43464  cncfperiod  43469