Theorem simp3rl 1245

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  omeu  8621  hashbclem  14487  ntrivcvgmul  15934  tsmsxp  24178  tgqioo  24835  ovolunlem2  25546  plyadd  26270  plymul  26271  coeeu  26278  nosupbnd1lem2  27768  noinfbnd1lem2  27783  tghilberti2  28660  cvmlift2lem10  35296  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem12  36079  lplnexllnN  39546  2llnjN  39549  4atlem12b  39593  lplncvrlvol2  39597  lncmp  39765  cdlema2N  39774  cdlemc2  40174  cdleme11a  40242  cdleme22eALTN  40327  cdleme24  40334  cdleme27a  40349  cdleme27N  40351  cdleme28  40355  cdlemefs29bpre0N  40398  cdlemefs29bpre1N  40399  cdlemefs29cpre1N  40400  cdlemefs29clN  40401  cdlemefs32fvaN  40404  cdlemefs32fva1  40405  cdleme36m  40443  cdleme39a  40447  cdleme17d3  40478  cdleme50trn2  40533  cdlemg36  40696  cdlemj3  40805  cdlemkfid1N  40903  cdlemkid1  40904  cdlemk19ylem  40912  cdlemk19xlem  40924  dihlsscpre  41216  dihord4  41240  dihatlat  41316  mapdh9a  41771  jm2.27  42996