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

Theorem 3impb 1178
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 602 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1176 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  3adant1l  1205  3adant1r  1206  3impdi  1268  vtocl3gf  3024  rspc2ev  3072  reuss  3621  frc  4675  trssord  4725  funtp  5460  resdif  5651  fnotovb  6120  fovrn  6224  fnovrn  6229  fmpt2co  6647  smoord  6814  odi  7008  oeoa  7026  oeoe  7028  nndi  7052  ecopovtrn  7193  ecovass  7202  ecovdi  7203  supmaxlem  7704  suppr  7708  harval2  8157  cdaassen  8341  fin23lem31  8502  tskuni  8940  addasspi  9054  mulasspi  9056  distrpi  9057  mulcanenq  9119  genpass  9168  distrlem1pr  9184  prlem934  9192  ltapr  9204  le2tri3i  9494  subadd  9603  addsub  9611  subdi  9768  submul2  9775  ltaddsub  9803  leaddsub  9805  divval  9986  div12  10006  diveq1  10015  divneg  10016  divdiv2  10033  ltmulgt11  10179  gt0div  10185  ge0div  10186  uzind3  10725  fnn0ind  10731  qdivcl  10964  irrmul  10968  xrlttr  11107  fzen  11456  modcyc  11729  modcyc2  11730  faclbnd4lem4  12058  cshweqdifid  12440  lenegsq  12794  moddvds  13527  dvdscmulr  13546  dvdsmulcr  13547  dvds2add  13549  dvds2sub  13550  dvdsleabs  13564  divalg  13592  divalgb  13593  ndvdsadd  13597  gcdcllem3  13682  dvdslegcd  13685  modgcd  13705  absmulgcd  13716  odzval  13848  pcmul  13903  ressid2  14211  ressval2  14212  catcisolem  14959  prf1st  14999  prf2nd  15000  1st2ndprf  15001  curfuncf  15033  curf2ndf  15042  pltval  15115  pospo  15128  lubel  15277  isdlat  15348  mndcl  15405  issubmnd  15434  prdsmndd  15439  submcl  15465  grpinvid1  15568  grpinvid2  15569  mulgp1  15635  ghmlin  15734  ghmsub  15737  odlem2  16024  gexlem2  16063  lsmvalx  16120  efgtval  16202  cmncom  16275  lssvnegcl  16961  islss3  16964  prdslmodd  16974  evlslem2  17527  zntoslem  17833  maducoeval2  18290  madutpos  18292  madugsum  18293  madurid  18294  unopn  18360  ntrss  18503  innei  18573  t1sep2  18817  metustsymOLD  19980  cncfi  20314  rrxds  20741  evlseu  21370  quotval  21645  abelthlem2  21784  mudivsum  22666  padicabv  22766  axsegconlem1  22988  grposn  23527  grpoinvid1  23542  grpoinvid2  23543  grpodivval  23555  gxval  23570  ablo4  23599  ablonncan  23606  issubgoi  23622  ablomul  23667  vcnegsubdi2  23778  nvnpcan  23865  nvmeq0  23869  nvabs  23886  imsdval  23902  ipval  23923  nmorepnf  23993  blo3i  24027  blometi  24028  ipasslem5  24060  hvmulcan  24299  his5  24313  his7  24317  his2sub2  24320  hhssnv  24490  fh1  24846  fh2  24847  cm2j  24848  homcl  24975  homco1  25030  homulass  25031  hoadddi  25032  hosubsub2  25041  braadd  25174  bramul  25175  lnopmul  25196  lnopli  25197  lnopaddmuli  25202  lnopsubmuli  25204  lnfnli  25269  lnfnaddmuli  25274  kbass2  25346  mdexchi  25564  xdivval  25919  resvid2  26152  resvval2  26153  unitdivcld  26187  signstfvc  26825  cvmlift2lem7  27048  finminlem  28359  ivthALT  28376  exidcl  28587  rngoneglmul  28603  rngonegrmul  28604  divrngcl  28609  crngocom  28647  crngm4  28649  inidl  28676  diophren  28999  monotoddzzfi  29130  rpexpmord  29136  ltrmynn0  29138  ltrmxnn0  29139  lermxnn0  29140  rmyeq  29144  lermy  29145  jm2.21  29190  dvconstbi  29455  expgrowth  29456  fnotaovb  29952  frgregordn0  30511  onetansqsecsq  30845  bi3impb  30928  eel132  31166  bnj229  31619  bnj546  31631  bnj570  31640  oposlem  32440  hlsuprexch  32638  ldilcnv  33372  ltrnu  33378  tgrpgrplem  34006  tgrpabl  34008  erngdvlem3  34247  erngdvlem3-rN  34255  dvalveclem  34283  dvhfvadd  34349  dvhgrp  34365  dvhlveclem  34366  djhval2  34657
  Copyright terms: Public domain W3C validator