Theorem simp3rl 1247

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

Assertion

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

Proof of Theorem simp3rl

Step	Hyp	Ref	Expression
1		simprl 770	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1135	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  8549  hashbclem  14417  ntrivcvgmul  15868  tsmsxp  24042  tgqioo  24688  ovolunlem2  25399  plyadd  26122  plymul  26123  coeeu  26130  nosupbnd1lem2  27621  noinfbnd1lem2  27636  tghilberti2  28565  cvmlift2lem10  35299  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem12  36086  lplnexllnN  39558  2llnjN  39561  4atlem12b  39605  lplncvrlvol2  39609  lncmp  39777  cdlema2N  39786  cdlemc2  40186  cdleme11a  40254  cdleme22eALTN  40339  cdleme24  40346  cdleme27a  40361  cdleme27N  40363  cdleme28  40367  cdlemefs29bpre0N  40410  cdlemefs29bpre1N  40411  cdlemefs29cpre1N  40412  cdlemefs29clN  40413  cdlemefs32fvaN  40416  cdlemefs32fva1  40417  cdleme36m  40455  cdleme39a  40459  cdleme17d3  40490  cdleme50trn2  40545  cdlemg36  40708  cdlemj3  40817  cdlemkfid1N  40915  cdlemkid1  40916  cdlemk19ylem  40924  cdlemk19xlem  40936  dihlsscpre  41228  dihord4  41252  dihatlat  41328  mapdh9a  41783  jm2.27  42997