Theorem simp3rl 1263

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  omeu  8569  hashbclem  14488  ntrivcvgmul  15955  tsmsxp  24280  tgqioo  24925  ovolunlem2  25625  plyadd  26342  plymul  26343  coeeu  26350  nosupbnd1lem2  27838  noinfbnd1lem2  27853  tghilberti2  28872  cvmlift2lem10  35702  btwnconn1lem1  36477  btwnconn1lem2  36478  btwnconn1lem12  36488  lplnexllnN  40227  2llnjN  40230  4atlem12b  40274  lplncvrlvol2  40278  lncmp  40446  cdlema2N  40455  cdlemc2  40855  cdleme11a  40923  cdleme22eALTN  41008  cdleme24  41015  cdleme27a  41030  cdleme27N  41032  cdleme28  41036  cdlemefs29bpre0N  41079  cdlemefs29bpre1N  41080  cdlemefs29cpre1N  41081  cdlemefs29clN  41082  cdlemefs32fvaN  41085  cdlemefs32fva1  41086  cdleme36m  41124  cdleme39a  41128  cdleme17d3  41159  cdleme50trn2  41214  cdlemg36  41377  cdlemj3  41486  cdlemkfid1N  41584  cdlemkid1  41585  cdlemk19ylem  41593  cdlemk19xlem  41605  dihlsscpre  41897  dihord4  41921  dihatlat  41997  mapdh9a  42452  jm2.27  43626