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  8586  hashbclem  14590  ntrivcvgmul  16064  tsmsxp  24467  tgqioo  25112  ovolunlem2  25812  plyadd  26529  plymul  26530  coeeu  26537  nosupbnd1lem2  28059  noinfbnd1lem2  28074  tghilberti2  29099  cvmlift2lem10  36056  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem12  36843  lplnexllnN  40601  2llnjN  40604  4atlem12b  40648  lplncvrlvol2  40652  lncmp  40820  cdlema2N  40829  cdlemc2  41229  cdleme11a  41297  cdleme22eALTN  41382  cdleme24  41389  cdleme27a  41404  cdleme27N  41406  cdleme28  41410  cdlemefs29bpre0N  41453  cdlemefs29bpre1N  41454  cdlemefs29cpre1N  41455  cdlemefs29clN  41456  cdlemefs32fvaN  41459  cdlemefs32fva1  41460  cdleme36m  41498  cdleme39a  41502  cdleme17d3  41533  cdleme50trn2  41588  cdlemg36  41751  cdlemj3  41860  cdlemkfid1N  41958  cdlemkid1  41959  cdlemk19ylem  41967  cdlemk19xlem  41979  dihlsscpre  42271  dihord4  42295  dihatlat  42371  mapdh9a  42826  jm2.27  43994