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

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

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 614 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1208 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  3adant1l  1268  3adant1r  1269  3impdi  1331  rsp2e  2858  vtocl3gf  3122  rspc2ev  3173  reuss  3736  frc  4819  trssord  5459  funtp  5653  resdif  5857  fnotovb  6356  fovrn  6466  fnovrn  6471  fmpt2co  6906  smoord  7110  odi  7306  oeoa  7324  oeoe  7326  nndi  7350  ecopovtrn  7492  ecovass  7496  ecovdi  7497  supmaxlemOLD  8008  suppr  8013  infpr  8045  harval2  8457  cdaassen  8638  fin23lem31  8799  tskuni  9234  addasspi  9346  mulasspi  9348  distrpi  9349  mulcanenq  9411  genpass  9460  distrlem1pr  9476  prlem934  9484  ltapr  9496  le2tri3i  9790  subadd  9904  addsub  9912  subdi  10080  submul2  10087  ltaddsub  10116  leaddsub  10118  divval  10300  div12  10320  diveq1  10329  divneg  10330  divdiv2  10347  ltmulgt11  10493  gt0div  10499  ge0div  10500  uzind3  11058  fnn0ind  11063  qdivcl  11314  irrmul  11318  xrlttr  11468  fzen  11845  modcyc  12164  modcyc2  12165  faclbnd4lem4  12513  cshweqdifid  12956  lenegsq  13432  moddvds  14361  dvdscmulr  14380  dvdsmulcr  14381  dvds2add  14383  dvds2sub  14384  dvdsleabs  14400  divalg  14433  divalgb  14434  ndvdsadd  14438  gcdcllem3  14524  dvdslegcd  14527  modgcd  14549  absmulgcd  14564  odzval  14785  odzvalOLD  14791  pcmul  14850  ressid2  15226  ressval2  15227  catcisolem  16050  prf1st  16138  prf2nd  16139  1st2ndprf  16140  curfuncf  16172  curf2ndf  16181  pltval  16255  pospo  16268  lubel  16417  isdlat  16488  issubmnd  16613  prdsmndd  16618  submcl  16649  grpinvid1  16763  grpinvid2  16764  mulgp1  16833  ghmlin  16937  ghmsub  16940  odlem2  17237  odlem2OLD  17253  gexlem2  17282  gexlem2OLD  17285  lsmvalx  17340  efgtval  17422  cmncom  17495  lssvnegcl  18228  islss3  18231  prdslmodd  18241  evlslem2  18784  evlseu  18788  zntoslem  19176  maducoeval2  19714  madutpos  19716  madugsum  19717  madurid  19718  m2cpminvid  19826  pm2mpghm  19889  unopn  19982  ntrss  20119  innei  20190  t1sep2  20434  metustsym  21619  cncfi  21975  rrxds  22401  quotval  23294  abelthlem2  23436  mudivsum  24417  padicabv  24517  axsegconlem1  24996  frgregordn0  25847  grposn  25992  grpoinvid1  26007  grpoinvid2  26008  grpodivval  26020  gxval  26035  ablo4  26064  ablonncan  26071  issubgoi  26087  ablomul  26132  vcnegsubdi2  26243  nvnpcan  26330  nvmeq0  26334  nvabs  26351  imsdval  26367  ipval  26388  nmorepnf  26458  blo3i  26492  blometi  26493  ipasslem5  26525  hvmulcan  26774  his5  26788  his7  26792  his2sub2  26795  hhssnv  26964  fh1  27320  fh2  27321  cm2j  27322  homcl  27448  homco1  27503  homulass  27504  hoadddi  27505  hosubsub2  27514  braadd  27647  bramul  27648  lnopmul  27669  lnopli  27670  lnopaddmuli  27675  lnopsubmuli  27677  lnfnli  27742  lnfnaddmuli  27747  kbass2  27819  mdexchi  28037  xdivval  28437  resvid2  28640  resvval2  28641  unitdivcld  28756  bnj229  29744  bnj546  29756  bnj570  29765  cvmlift2lem7  30081  finminlem  31023  ivthALT  31040  topdifinffinlem  31795  exidcl  32219  rngoneglmul  32235  rngonegrmul  32236  divrngcl  32241  crngocom  32279  crngm4  32281  inidl  32308  oposlem  32793  hlsuprexch  32991  ldilcnv  33725  ltrnu  33731  tgrpgrplem  34361  tgrpabl  34363  erngdvlem3  34602  erngdvlem3-rN  34610  dvalveclem  34638  dvhfvadd  34704  dvhgrp  34720  dvhlveclem  34721  djhval2  35012  diophren  35701  monotoddzzfi  35835  rpexpmord  35841  ltrmynn0  35843  ltrmxnn0  35844  lermxnn0  35845  rmyeq  35849  lermy  35850  jm2.21  35894  radcnvrat  36707  dvconstbi  36727  expgrowth  36728  bi3impb  36883  eel132  37124  fnotaovb  38738  ccatpfx  38990  submgmcl  40067  onetansqsecsq  40754
  Copyright terms: Public domain W3C validator