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 782	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1153	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  omeu  8571  hashbclem  14491  ntrivcvgmul  15958  tsmsxp  24293  tgqioo  24938  ovolunlem2  25638  plyadd  26355  plymul  26356  coeeu  26363  nosupbnd1lem2  27854  noinfbnd1lem2  27869  tghilberti2  28892  cvmlift2lem10  35785  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem12  36571  lplnexllnN  40319  2llnjN  40322  4atlem12b  40366  lplncvrlvol2  40370  lncmp  40538  cdlema2N  40547  cdlemc2  40947  cdleme11a  41015  cdleme22eALTN  41100  cdleme24  41107  cdleme27a  41122  cdleme27N  41124  cdleme28  41128  cdlemefs29bpre0N  41171  cdlemefs29bpre1N  41172  cdlemefs29cpre1N  41173  cdlemefs29clN  41174  cdlemefs32fvaN  41177  cdlemefs32fva1  41178  cdleme36m  41216  cdleme39a  41220  cdleme17d3  41251  cdleme50trn2  41306  cdlemg36  41469  cdlemj3  41578  cdlemkfid1N  41676  cdlemkid1  41677  cdlemk19ylem  41685  cdlemk19xlem  41697  dihlsscpre  41989  dihord4  42013  dihatlat  42089  mapdh9a  42544  jm2.27  43718