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  8513  hashbclem  14405  ntrivcvgmul  15858  tsmsxp  24130  tgqioo  24775  ovolunlem2  25475  plyadd  26192  plymul  26193  coeeu  26200  nosupbnd1lem2  27687  noinfbnd1lem2  27702  tghilberti2  28720  cvmlift2lem10  35510  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem12  36296  lplnexllnN  40024  2llnjN  40027  4atlem12b  40071  lplncvrlvol2  40075  lncmp  40243  cdlema2N  40252  cdlemc2  40652  cdleme11a  40720  cdleme22eALTN  40805  cdleme24  40812  cdleme27a  40827  cdleme27N  40829  cdleme28  40833  cdlemefs29bpre0N  40876  cdlemefs29bpre1N  40877  cdlemefs29cpre1N  40878  cdlemefs29clN  40879  cdlemefs32fvaN  40882  cdlemefs32fva1  40883  cdleme36m  40921  cdleme39a  40925  cdleme17d3  40956  cdleme50trn2  41011  cdlemg36  41174  cdlemj3  41283  cdlemkfid1N  41381  cdlemkid1  41382  cdlemk19ylem  41390  cdlemk19xlem  41402  dihlsscpre  41694  dihord4  41718  dihatlat  41794  mapdh9a  42249  jm2.27  43454