Theorem simp3rl 1248

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 1137	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  omeu  8291  hashbclem  13981  ntrivcvgmul  15429  tsmsxp  23006  tgqioo  23651  ovolunlem2  24349  plyadd  25065  plymul  25066  coeeu  25073  tghilberti2  26683  cvmlift2lem10  32941  nosupbnd1lem2  33598  noinfbnd1lem2  33613  btwnconn1lem1  34075  btwnconn1lem2  34076  btwnconn1lem12  34086  lplnexllnN  37264  2llnjN  37267  4atlem12b  37311  lplncvrlvol2  37315  lncmp  37483  cdlema2N  37492  cdlemc2  37892  cdleme11a  37960  cdleme22eALTN  38045  cdleme24  38052  cdleme27a  38067  cdleme27N  38069  cdleme28  38073  cdlemefs29bpre0N  38116  cdlemefs29bpre1N  38117  cdlemefs29cpre1N  38118  cdlemefs29clN  38119  cdlemefs32fvaN  38122  cdlemefs32fva1  38123  cdleme36m  38161  cdleme39a  38165  cdleme17d3  38196  cdleme50trn2  38251  cdlemg36  38414  cdlemj3  38523  cdlemkfid1N  38621  cdlemkid1  38622  cdlemk19ylem  38630  cdlemk19xlem  38642  dihlsscpre  38934  dihord4  38958  dihatlat  39034  mapdh9a  39489  jm2.27  40474