Theorem simp3rl 1134

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

Assertion

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

Proof of Theorem simp3rl

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

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

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 1039

This theorem is referenced by:  omeu  7665  hashbclem  13236  ntrivcvgmul  14634  tsmsxp  21958  tgqioo  22603  ovolunlem2  23266  plyadd  23973  plymul  23974  coeeu  23981  tghilberti2  25533  cvmlift2lem10  31294  nosupbnd1lem2  31855  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem12  32205  lplnexllnN  34850  2llnjN  34853  4atlem12b  34897  lplncvrlvol2  34901  lncmp  35069  cdlema2N  35078  cdlemc2  35479  cdleme11a  35547  cdleme22eALTN  35633  cdleme24  35640  cdleme27a  35655  cdleme27N  35657  cdleme28  35661  cdlemefs29bpre0N  35704  cdlemefs29bpre1N  35705  cdlemefs29cpre1N  35706  cdlemefs29clN  35707  cdlemefs32fvaN  35710  cdlemefs32fva1  35711  cdleme36m  35749  cdleme39a  35753  cdleme17d3  35784  cdleme50trn2  35839  cdlemg36  36002  cdlemj3  36111  cdlemkfid1N  36209  cdlemkid1  36210  cdlemk19ylem  36218  cdlemk19xlem  36230  dihlsscpre  36523  dihord4  36547  dihatlat  36623  mapdh9a  37079  jm2.27  37575