Theorem simp3rl 1127

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  omeu  7552  hashbclem  13093  ntrivcvgmul  14473  tsmsxp  21768  tgqioo  22411  ovolunlem2  23073  plyadd  23777  plymul  23778  coeeu  23785  tghilberti2  25333  cvmlift2lem10  30548  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem12  31375  lplnexllnN  33868  2llnjN  33871  4atlem12b  33915  lplncvrlvol2  33919  lncmp  34087  cdlema2N  34096  cdlemc2  34497  cdleme11a  34565  cdleme22eALTN  34651  cdleme24  34658  cdleme27a  34673  cdleme27N  34675  cdleme28  34679  cdlemefs29bpre0N  34722  cdlemefs29bpre1N  34723  cdlemefs29cpre1N  34724  cdlemefs29clN  34725  cdlemefs32fvaN  34728  cdlemefs32fva1  34729  cdleme36m  34767  cdleme39a  34771  cdleme17d3  34802  cdleme50trn2  34857  cdlemg36  35020  cdlemj3  35129  cdlemkfid1N  35227  cdlemkid1  35228  cdlemk19ylem  35236  cdlemk19xlem  35248  dihlsscpre  35541  dihord4  35565  dihatlat  35641  mapdh9a  36097  jm2.27  36593