Theorem simp3rl 1265

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

Assertion

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

Proof of Theorem simp3rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  omeu  8631  hashbclem  14638  ntrivcvgmul  16115  tsmsxp  24529  tgqioo  25174  ovolunlem2  25874  plyadd  26591  plymul  26592  coeeu  26599  nosupbnd1lem2  28123  noinfbnd1lem2  28138  tghilberti2  29163  cvmlift2lem10  36285  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem12  37078  lplnexllnN  40887  2llnjN  40890  4atlem12b  40934  lplncvrlvol2  40938  lncmp  41106  cdlema2N  41115  cdlemc2  41515  cdleme11a  41583  cdleme22eALTN  41668  cdleme24  41675  cdleme27a  41690  cdleme27N  41692  cdleme28  41696  cdlemefs29bpre0N  41739  cdlemefs29bpre1N  41740  cdlemefs29cpre1N  41741  cdlemefs29clN  41742  cdlemefs32fvaN  41745  cdlemefs32fva1  41746  cdleme36m  41784  cdleme39a  41788  cdleme17d3  41819  cdleme50trn2  41874  cdlemg36  42037  cdlemj3  42146  cdlemkfid1N  42244  cdlemkid1  42245  cdlemk19ylem  42253  cdlemk19xlem  42265  dihlsscpre  42557  dihord4  42581  dihatlat  42657  mapdh9a  43112  jm2.27  44281