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

Theorem 3impb 1147
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant1l  1174  3adant1r  1175  3impdi  1237  vtocl3gf  2859  rspc2ev  2905  reuss  3462  frc  4375  trssord  4425  funtp  5319  resdif  5510  fnotovb  5910  fovrn  6006  fnovrn  6011  fmpt2co  6218  smoord  6398  odi  6593  oeoa  6611  oeoe  6613  nndi  6637  ecopovtrn  6777  ecovass  6786  ecovdi  6787  supmaxlem  7231  suppr  7235  harval2  7646  cdaassen  7824  fin23lem31  7985  tskuni  8421  addasspi  8535  mulasspi  8537  distrpi  8538  mulcanenq  8600  genpass  8649  distrlem1pr  8665  prlem934  8673  ltapr  8685  le2tri3i  8965  subadd  9070  addsub  9078  subdi  9229  submul2  9236  ltaddsub  9264  leaddsub  9266  divval  9442  div12  9462  diveq1  9470  divneg  9471  divdiv2  9488  ltmulgt11  9632  gt0div  9638  ge0div  9639  uzind3  10121  fnn0ind  10127  qdivcl  10353  irrmul  10357  xrlttr  10490  fzen  10827  modcyc  11015  modcyc2  11016  faclbnd4lem4  11325  lenegsq  11820  moddvds  12554  dvdscmulr  12573  dvdsmulcr  12574  dvds2add  12576  dvds2sub  12577  dvdsleabs  12591  divalg  12618  divalgb  12619  ndvdsadd  12623  gcdcllem3  12708  dvdslegcd  12711  modgcd  12731  absmulgcd  12742  odzval  12872  pcmul  12920  ressid2  13212  ressval2  13213  catcisolem  13954  prf1st  13994  prf2nd  13995  1st2ndprf  13996  curfuncf  14028  curf2ndf  14037  pltval  14110  pospo  14123  joinval  14138  joinval2  14139  meetval  14145  meetval2  14146  lubel  14242  isdlat  14312  spwpr4  14356  laspwcl  14359  lanfwcl  14360  mndcl  14388  issubmnd  14417  prdsmndd  14421  submcl  14446  grpinvid1  14546  grpinvid2  14547  mulgp1  14609  ghmlin  14704  ghmsub  14707  odlem2  14870  gexlem2  14909  lsmvalx  14966  efgtval  15048  cmncom  15121  lssvnegcl  15729  islss3  15732  prdslmodd  15742  evlslem2  16265  zntoslem  16526  unopn  16665  ntrss  16808  innei  16878  t1sep2  17113  cncfi  18414  evlseu  19416  quotval  19688  abelthlem2  19824  mudivsum  20695  padicabv  20795  grposn  20898  grpoinvid1  20913  grpoinvid2  20914  grpodivval  20926  gxval  20941  ablo4  20970  ablonncan  20977  issubgoi  20993  ablomul  21038  vcnegsubdi2  21147  nvnpcan  21234  nvmeq0  21238  nvabs  21255  imsdval  21271  ipval  21292  nmorepnf  21362  blo3i  21396  blometi  21397  ipasslem5  21429  hvmulcan  21667  his5  21681  his7  21685  his2sub2  21688  hhssnv  21857  fh1  22213  fh2  22214  cm2j  22215  homcl  22342  homco1  22397  homulass  22398  hoadddi  22399  hosubsub2  22408  braadd  22541  bramul  22542  lnopmul  22563  lnopli  22564  lnopaddmuli  22569  lnopsubmuli  22571  lnfnli  22636  lnfnaddmuli  22641  kbass2  22713  mdexchi  22931  xdivval  23118  unitdivcld  23300  cvmlift2lem7  23855  axsegconlem1  24617  subaddv  25774  cmp2morp  26061  finminlem  26334  ivthALT  26361  lpss2  26571  exidcl  26669  rngoneglmul  26685  rngonegrmul  26686  divrngcl  26691  crngocom  26729  crngm4  26731  inidl  26758  diophren  26999  monotoddzzfi  27130  rpexpmord  27136  ltrmynn0  27138  ltrmxnn0  27139  lermxnn0  27140  rmyeq  27144  lermy  27145  jm2.21  27190  unxpwdom3  27359  dvconstbi  27654  expgrowth  27655  fnotaovb  28166  onetansqsecsq  28485  bi3impb  28547  eel132  28780  bnj229  29232  bnj546  29244  bnj570  29253  oposlem  29995  hlsuprexch  30192  ldilcnv  30926  ltrnu  30932  tgrpgrplem  31560  tgrpabl  31562  erngdvlem3  31801  erngdvlem3-rN  31809  dvalveclem  31837  dvhfvadd  31903  dvhgrp  31919  dvhlveclem  31920  djhval2  32211
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator