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

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

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 475 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054 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 385  df-3an 1056 This theorem is referenced by:  3simpb  1079  3simpc  1080  simp1  1081  simp2  1082  3adant3  1101  3adantl3  1239  3adantr3  1242  disjtp2  4284  pr1eqbg  4421  otel3xp  5187  brcogw  5323  funtpg  5980  funtpgOLD  5981  ftpg  6463  ovig  6824  el2xptp0  7256  wfrlem17  7476  undifixp  7986  tz9.1c  8644  ackbij1lem16  9095  enqeq  9794  prlem934  9893  lt2halves  11305  nn0n0n1ge2  11396  ixxssixx  12227  ltdifltdiv  12675  hash2prd  13295  hashtpg  13305  2swrdeqwrdeq  13499  swrd0swrd0  13509  swrdccatid  13543  s3eq3seq  13730  sumtp  14522  dvdscmulr  15057  dvdsmulcr  15058  dvds2add  15062  dvds2sub  15063  dvdstr  15065  vdwlem12  15743  cshwsidrepswmod0  15848  cshwshashlem2  15850  setsstructOLD  15946  initoeu2lem0  16710  estrreslem1  16824  funcestrcsetclem9  16835  funcsetcestrclem9  16850  sgrp2nmndlem4  17462  dfgrp3e  17562  lmhmlem  19077  psgndiflemA  19995  mpt2frlmd  20164  matsc  20304  scmatrhmcl  20382  mdetdiaglem  20452  decpmatid  20623  decpmatmullem  20624  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  cpmidgsumm2pm  20722  cpmidpmat  20726  cpmadumatpoly  20736  2ndcctbss  21306  dvfsumrlim  23839  dvfsumrlim2  23840  ulmval  24179  relogbmul  24560  axcontlem2  25890  funvtxvalOLD  25952  funiedgvalOLD  25953  uspgr1v1eop  26186  uhgrissubgr  26212  subgrprop3  26213  0uhgrsubgr  26216  wlkelwrd  26584  uhgrwkspth  26707  usgr2wlkspth  26711  2pthon3v  26908  clwwlknonex2e  27085  uhgr3cyclex  27160  umgr3v3e3cycl  27162  numclwlk1lem2foa  27344  numclwwlk5  27375  leopmul  29121  strlem3a  29239  0elsiga  30305  afsval  30877  bnj999  31153  conway  32035  cgr3permute3  32279  cgr3com  32285  colineardim1  32293  brofs2  32309  brifs2  32310  btwnconn1lem4  32322  btwnconn1lem5  32323  btwnconn1lem6  32324  midofsegid  32336  isbasisrelowllem1  33333  isbasisrelowllem2  33334  icoreclin  33335  ftc1anclem8  33622  sdclem2  33668  ismndo1  33802  lsmcv2  34634  lvolnleat  35187  paddasslem14  35437  4atexlemswapqr  35667  isltrn2N  35724  cdlemftr1  36172  cdlemg5  36210  iocinico  38114  pwinfi2  38184  relexpxpnnidm  38312  sigaras  41365  sigarms  41366  pfxsuffeqwrdeq  41731  pfxccatpfx1  41752  pfxccatpfx2  41753  even3prm2  41953  bgoldbtbndlem4  42021  bgoldbtbnd  42022  mhmismgmhm  42131  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  gsumlsscl  42489  ldepspr  42587  lincresunit3lem3  42588  lincresunit3lem1  42593  lincresunit3  42595
 Copyright terms: Public domain W3C validator