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

Theorem 3impb 1183
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1181 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  3adant1l  1210  3adant1r  1211  3impdi  1273  vtocl3gf  3028  rspc2ev  3076  reuss  3626  frc  4681  trssord  4731  funtp  5465  resdif  5656  fnotovb  6124  fovrn  6228  fnovrn  6233  fmpt2co  6651  smoord  6818  odi  7010  oeoa  7028  oeoe  7030  nndi  7054  ecopovtrn  7195  ecovass  7204  ecovdi  7205  supmaxlem  7706  suppr  7710  harval2  8159  cdaassen  8343  fin23lem31  8504  tskuni  8942  addasspi  9056  mulasspi  9058  distrpi  9059  mulcanenq  9121  genpass  9170  distrlem1pr  9186  prlem934  9194  ltapr  9206  le2tri3i  9496  subadd  9605  addsub  9613  subdi  9770  submul2  9777  ltaddsub  9805  leaddsub  9807  divval  9988  div12  10008  diveq1  10017  divneg  10018  divdiv2  10035  ltmulgt11  10181  gt0div  10187  ge0div  10188  uzind3  10727  fnn0ind  10733  qdivcl  10966  irrmul  10970  xrlttr  11109  fzen  11459  modcyc  11735  modcyc2  11736  faclbnd4lem4  12064  cshweqdifid  12446  lenegsq  12800  moddvds  13534  dvdscmulr  13553  dvdsmulcr  13554  dvds2add  13556  dvds2sub  13557  dvdsleabs  13571  divalg  13599  divalgb  13600  ndvdsadd  13604  gcdcllem3  13689  dvdslegcd  13692  modgcd  13712  absmulgcd  13723  odzval  13855  pcmul  13910  ressid2  14218  ressval2  14219  catcisolem  14966  prf1st  15006  prf2nd  15007  1st2ndprf  15008  curfuncf  15040  curf2ndf  15049  pltval  15122  pospo  15135  lubel  15284  isdlat  15355  mndcl  15412  issubmnd  15441  prdsmndd  15446  submcl  15472  grpinvid1  15577  grpinvid2  15578  mulgp1  15644  ghmlin  15743  ghmsub  15746  odlem2  16033  gexlem2  16072  lsmvalx  16129  efgtval  16211  cmncom  16284  lssvnegcl  17014  islss3  17017  prdslmodd  17027  evlslem2  17572  evlseu  17577  zntoslem  17964  maducoeval2  18421  madutpos  18423  madugsum  18424  madurid  18425  unopn  18491  ntrss  18634  innei  18704  t1sep2  18948  metustsymOLD  20111  cncfi  20445  rrxds  20872  quotval  21733  abelthlem2  21872  mudivsum  22754  padicabv  22854  axsegconlem1  23114  grposn  23653  grpoinvid1  23668  grpoinvid2  23669  grpodivval  23681  gxval  23696  ablo4  23725  ablonncan  23732  issubgoi  23748  ablomul  23793  vcnegsubdi2  23904  nvnpcan  23991  nvmeq0  23995  nvabs  24012  imsdval  24028  ipval  24049  nmorepnf  24119  blo3i  24153  blometi  24154  ipasslem5  24186  hvmulcan  24425  his5  24439  his7  24443  his2sub2  24446  hhssnv  24616  fh1  24972  fh2  24973  cm2j  24974  homcl  25101  homco1  25156  homulass  25157  hoadddi  25158  hosubsub2  25167  braadd  25300  bramul  25301  lnopmul  25322  lnopli  25323  lnopaddmuli  25328  lnopsubmuli  25330  lnfnli  25395  lnfnaddmuli  25400  kbass2  25472  mdexchi  25690  xdivval  26045  resvid2  26248  resvval2  26249  unitdivcld  26283  signstfvc  26927  cvmlift2lem7  27150  finminlem  28466  ivthALT  28483  exidcl  28694  rngoneglmul  28710  rngonegrmul  28711  divrngcl  28716  crngocom  28754  crngm4  28756  inidl  28783  diophren  29105  monotoddzzfi  29236  rpexpmord  29242  ltrmynn0  29244  ltrmxnn0  29245  lermxnn0  29246  rmyeq  29250  lermy  29251  jm2.21  29296  dvconstbi  29561  expgrowth  29562  fnotaovb  30057  frgregordn0  30616  onetansqsecsq  30985  bi3impb  31074  eel132  31311  bnj229  31764  bnj546  31776  bnj570  31785  oposlem  32667  hlsuprexch  32865  ldilcnv  33599  ltrnu  33605  tgrpgrplem  34233  tgrpabl  34235  erngdvlem3  34474  erngdvlem3-rN  34482  dvalveclem  34510  dvhfvadd  34576  dvhgrp  34592  dvhlveclem  34593  djhval2  34884
  Copyright terms: Public domain W3C validator