MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3rl Structured version   Visualization version   GIF version

Theorem simp3rl 1243
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3rl ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 770 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1132 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 1086
This theorem is referenced by:  omeu  8198  hashbclem  13810  ntrivcvgmul  15254  tsmsxp  22764  tgqioo  23409  ovolunlem2  24106  plyadd  24818  plymul  24819  coeeu  24826  tghilberti2  26436  cvmlift2lem10  32673  nosupbnd1lem2  33323  btwnconn1lem1  33662  btwnconn1lem2  33663  btwnconn1lem12  33673  lplnexllnN  36859  2llnjN  36862  4atlem12b  36906  lplncvrlvol2  36910  lncmp  37078  cdlema2N  37087  cdlemc2  37487  cdleme11a  37555  cdleme22eALTN  37640  cdleme24  37647  cdleme27a  37662  cdleme27N  37664  cdleme28  37668  cdlemefs29bpre0N  37711  cdlemefs29bpre1N  37712  cdlemefs29cpre1N  37713  cdlemefs29clN  37714  cdlemefs32fvaN  37717  cdlemefs32fva1  37718  cdleme36m  37756  cdleme39a  37760  cdleme17d3  37791  cdleme50trn2  37846  cdlemg36  38009  cdlemj3  38118  cdlemkfid1N  38216  cdlemkid1  38217  cdlemk19ylem  38225  cdlemk19xlem  38237  dihlsscpre  38529  dihord4  38553  dihatlat  38629  mapdh9a  39084  jm2.27  39942
  Copyright terms: Public domain W3C validator