Theorem simp3rl 1248

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

Assertion

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

Proof of Theorem simp3rl

Step	Hyp	Ref	Expression
1		simprl 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1136	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  omeu  8520  hashbclem  14414  ntrivcvgmul  15867  tsmsxp  24120  tgqioo  24765  ovolunlem2  25465  plyadd  26182  plymul  26183  coeeu  26190  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28706  cvmlift2lem10  35494  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem12  36280  lplnexllnN  40010  2llnjN  40013  4atlem12b  40057  lplncvrlvol2  40061  lncmp  40229  cdlema2N  40238  cdlemc2  40638  cdleme11a  40706  cdleme22eALTN  40791  cdleme24  40798  cdleme27a  40813  cdleme27N  40815  cdleme28  40819  cdlemefs29bpre0N  40862  cdlemefs29bpre1N  40863  cdlemefs29cpre1N  40864  cdlemefs29clN  40865  cdlemefs32fvaN  40868  cdlemefs32fva1  40869  cdleme36m  40907  cdleme39a  40911  cdleme17d3  40942  cdleme50trn2  40997  cdlemg36  41160  cdlemj3  41269  cdlemkfid1N  41367  cdlemkid1  41368  cdlemk19ylem  41376  cdlemk19xlem  41388  dihlsscpre  41680  dihord4  41704  dihatlat  41780  mapdh9a  42235  jm2.27  43436