Theorem simp3rl 1132

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  omeu  7610  hashbclem  13174  ntrivcvgmul  14559  tsmsxp  21868  tgqioo  22511  ovolunlem2  23173  plyadd  23877  plymul  23878  coeeu  23885  tghilberti2  25433  cvmlift2lem10  31002  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem12  31847  lplnexllnN  34330  2llnjN  34333  4atlem12b  34377  lplncvrlvol2  34381  lncmp  34549  cdlema2N  34558  cdlemc2  34959  cdleme11a  35027  cdleme22eALTN  35113  cdleme24  35120  cdleme27a  35135  cdleme27N  35137  cdleme28  35141  cdlemefs29bpre0N  35184  cdlemefs29bpre1N  35185  cdlemefs29cpre1N  35186  cdlemefs29clN  35187  cdlemefs32fvaN  35190  cdlemefs32fva1  35191  cdleme36m  35229  cdleme39a  35233  cdleme17d3  35264  cdleme50trn2  35319  cdlemg36  35482  cdlemj3  35591  cdlemkfid1N  35689  cdlemkid1  35690  cdlemk19ylem  35698  cdlemk19xlem  35710  dihlsscpre  36003  dihord4  36027  dihatlat  36103  mapdh9a  36559  jm2.27  37055