Theorem simp3rl 1242

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  omeu  8211  hashbclem  13811  ntrivcvgmul  15258  tsmsxp  22763  tgqioo  23408  ovolunlem2  24099  plyadd  24807  plymul  24808  coeeu  24815  tghilberti2  26424  cvmlift2lem10  32559  nosupbnd1lem2  33209  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem12  33559  lplnexllnN  36715  2llnjN  36718  4atlem12b  36762  lplncvrlvol2  36766  lncmp  36934  cdlema2N  36943  cdlemc2  37343  cdleme11a  37411  cdleme22eALTN  37496  cdleme24  37503  cdleme27a  37518  cdleme27N  37520  cdleme28  37524  cdlemefs29bpre0N  37567  cdlemefs29bpre1N  37568  cdlemefs29cpre1N  37569  cdlemefs29clN  37570  cdlemefs32fvaN  37573  cdlemefs32fva1  37574  cdleme36m  37612  cdleme39a  37616  cdleme17d3  37647  cdleme50trn2  37702  cdlemg36  37865  cdlemj3  37974  cdlemkfid1N  38072  cdlemkid1  38073  cdlemk19ylem  38081  cdlemk19xlem  38093  dihlsscpre  38385  dihord4  38409  dihatlat  38485  mapdh9a  38940  jm2.27  39625