MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impa Structured version   Unicode version

Theorem 3impa 1192
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3impa  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 604 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1191 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 185  df-an 371  df-3an 976
This theorem is referenced by:  3impdir  1285  syl3an9b  1298  biimp3a  1329  stoic3  1596  rspec3  2816  rspc3v  3208  raltpg  4065  rextpg  4066  disjiun  4427  3optocl  5068  fun2ssres  5619  funssfv  5871  foco2  6036  f1elima  6156  ot1stg  6799  ot2ndg  6800  smogt  7040  omord2  7218  omword  7221  oeword  7241  omabslem  7297  ecovass  7420  fpmg  7446  findcard  7761  cdaun  8555  cfsmolem  8653  ingru  9196  addasspi  9276  mulasspi  9278  ltapi  9284  ltmpi  9285  axpre-ltadd  9547  leltne  9677  dedekind  9747  recextlem2  10187  divdiv32  10259  divdiv1  10262  lble  10502  fnn0ind  10969  supminf  11179  xrleltne  11361  xrmaxeq  11390  xrmineq  11391  iccgelb  11591  elicc4  11601  iccsplit  11663  elfz  11688  fzrevral  11773  modabs  12010  expgt0  12180  expge0  12183  expge1  12184  mulexpz  12187  expp1z  12195  expm1  12196  digit1  12281  faclbnd4  12356  faclbnd5  12357  ccatval1  12576  abssubne0  13130  binom  13623  dvds0lem  13975  dvdsnegb  13982  muldvds1  13989  muldvds2  13990  dvdscmulr  13993  dvdsmulcr  13994  gcdaddm  14148  prmdvdsexp  14236  rpexp1i  14243  monpropd  15113  prfval  15446  xpcpropd  15455  curf2ndf  15494  eqglact  16230  mndodcongi  16545  oddvdsnn0  16546  efgi0  16716  efgi1  16717  lss0cl  17571  scmatscmid  18985  pmatcollpw3fi1lem1  19264  cnpval  19714  cnf2  19727  cnnei  19760  lfinun  20003  ptpjcn  20089  cnmptk2  20164  flfval  20468  cnmpt2plusg  20564  cnmpt2vsca  20674  ustincl  20687  xbln0  20894  blssec  20915  blpnfctr  20916  mopni2  20973  mopni3  20974  nmoval  21199  nmocl  21204  isnghm2  21208  isnmhm2  21236  cnmpt2ds  21325  metdseq0  21335  cnmpt2ip  21665  caucfil  21699  mbfimasn  22018  dvnf  22307  dvnbss  22308  coemul  22625  dvply1  22656  dvnply2  22659  pserdvlem2  22799  logeftb  22944  advlogexp  23012  cxpne0  23034  cxpp1  23037  lgsne0  23584  f1otrg  24150  ax5seglem9  24216  umgrass  24295  umgran0  24296  umgrale  24297  nbgraf1olem3  24419  pthdepisspth  24552  grposn  25193  sspval  25612  sspnval  25626  lnof  25646  nmooval  25654  nmooge0  25658  nmoub3i  25664  bloln  25675  nmblore  25677  hosval  26635  homval  26636  hodval  26637  hfsval  26638  hfmval  26639  homulass  26697  hoadddir  26699  nmopub2tALT  26804  nmfnleub2  26821  kbval  26849  lnopmul  26862  0lnfn  26880  lnopcoi  26898  nmcoplb  26925  nmcfnlb  26949  kbass2  27012  nmopleid  27034  hstoh  27127  mdi  27190  dmdi  27197  dmdi4  27202  supxrnemnf  27559  reofld  27807  elno2  29389  ftc1anclem2  30066  fzmul  30208  nninfnub  30219  exidreslem  30314  ghomf  30319  rngohomf  30344  rngohom1  30346  rngohomadd  30347  rngohommul  30348  rngoiso1o  30357  rngoisohom  30358  igenmin  30436  3anrabdioph  30691  3orrabdioph  30692  rencldnfilem  30729  expmordi  30858  divalgmodcl  30904  jm2.18  30905  jm2.25  30916  jm2.15nn0  30920  lcmdvds  31190  addrfv  31332  subrfv  31333  mulvfv  31334  ssfiunibd  31458  stoweidlem34  31705  stoweidlem48  31719  aovmpt4g  32124  bi3impa  32986  ex3  33077  bnj605  33698  bnj607  33707  bnj1097  33770  lkrcl  34557  lkrf0  34558  omlfh1N  34723  tendoex  36441
  Copyright terms: Public domain W3C validator