Theorem simp3rl 1247

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  omeu  8623  hashbclem  14491  ntrivcvgmul  15938  tsmsxp  24163  tgqioo  24821  ovolunlem2  25533  plyadd  26256  plymul  26257  coeeu  26264  nosupbnd1lem2  27754  noinfbnd1lem2  27769  tghilberti2  28646  cvmlift2lem10  35317  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem12  36099  lplnexllnN  39566  2llnjN  39569  4atlem12b  39613  lplncvrlvol2  39617  lncmp  39785  cdlema2N  39794  cdlemc2  40194  cdleme11a  40262  cdleme22eALTN  40347  cdleme24  40354  cdleme27a  40369  cdleme27N  40371  cdleme28  40375  cdlemefs29bpre0N  40418  cdlemefs29bpre1N  40419  cdlemefs29cpre1N  40420  cdlemefs29clN  40421  cdlemefs32fvaN  40424  cdlemefs32fva1  40425  cdleme36m  40463  cdleme39a  40467  cdleme17d3  40498  cdleme50trn2  40553  cdlemg36  40716  cdlemj3  40825  cdlemkfid1N  40923  cdlemkid1  40924  cdlemk19ylem  40932  cdlemk19xlem  40944  dihlsscpre  41236  dihord4  41260  dihatlat  41336  mapdh9a  41791  jm2.27  43020