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

Theorem 3simpa 1056
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpa ((𝜑𝜓𝜒) → (𝜑𝜓))

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 1038 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 476 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 1038
This theorem is referenced by:  3simpb  1057  3simpc  1058  simp1  1059  simp2  1060  3adant3  1079  3adantl3  1217  3adantr3  1220  disjtp2  4224  pr1eqbg  4360  otel3xp  5115  brcogw  5252  funtpg  5902  funtpgOLD  5903  ftpg  6380  ovig  6738  el2xptp0  7160  wfrlem17  7379  undifixp  7891  tz9.1c  8553  ackbij1lem16  9004  enqeq  9703  prlem934  9802  lt2halves  11214  nn0n0n1ge2  11305  ixxssixx  12134  ltdifltdiv  12578  hash2prd  13198  hashtpg  13208  2swrdeqwrdeq  13394  swrd0swrd0  13404  swrdccatid  13437  sumtp  14411  dvdscmulr  14937  dvdsmulcr  14938  dvds2add  14942  dvds2sub  14943  dvdstr  14945  vdwlem12  15623  cshwsidrepswmod0  15728  cshwshashlem2  15730  setsstructOLD  15823  initoeu2lem0  16587  estrreslem1  16701  funcestrcsetclem9  16712  funcsetcestrclem9  16727  sgrp2nmndlem4  17339  dfgrp3e  17439  lmhmlem  18951  psgndiflemA  19869  mpt2frlmd  20038  matsc  20178  scmatrhmcl  20256  mdetdiaglem  20326  decpmatid  20497  decpmatmullem  20498  mp2pm2mplem4  20536  chfacfisf  20581  chfacfisfcpmat  20582  cpmidgsumm2pm  20596  cpmidpmat  20600  cpmadumatpoly  20610  2ndcctbss  21171  dvfsumrlim  23705  dvfsumrlim2  23706  ulmval  24045  relogbmul  24422  axcontlem2  25752  funvtxvalOLD  25814  funiedgvalOLD  25815  uspgr1v1eop  26041  uhgrissubgr  26067  subgrprop3  26068  0uhgrsubgr  26071  wlkelwrd  26405  uhgrwkspth  26527  usgr2wlkspth  26531  wwlknbp2  26628  2pthon3v  26715  uhgr3cyclex  26915  umgr3v3e3cycl  26917  numclwwlk5  27107  leopmul  28854  strlem3a  28972  0elsiga  29970  afsval  30477  bnj999  30756  cgr3permute3  31817  cgr3com  31823  colineardim1  31831  brofs2  31847  brifs2  31848  btwnconn1lem4  31860  btwnconn1lem5  31861  btwnconn1lem6  31862  midofsegid  31874  isbasisrelowllem1  32856  isbasisrelowllem2  32857  icoreclin  32858  ftc1anclem8  33145  sdclem2  33191  ismndo1  33325  lsmcv2  33817  lvolnleat  34370  paddasslem14  34620  4atexlemswapqr  34850  isltrn2N  34907  cdlemftr1  35356  cdlemg5  35394  iocinico  37299  pwinfi2  37369  relexpxpnnidm  37497  sigaras  40364  sigarms  40365  pfxsuffeqwrdeq  40721  pfxccatpfx1  40742  pfxccatpfx2  40743  bgoldbtbndlem4  41001  bgoldbtbnd  41002  mhmismgmhm  41110  funcringcsetcALTV2lem9  41348  funcringcsetclem9ALTV  41371  gsumlsscl  41468  ldepspr  41566  lincresunit3lem3  41567  lincresunit3lem1  41572  lincresunit3  41574
  Copyright terms: Public domain W3C validator