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

Theorem 3impb 1149
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1147 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant1l  1176  3adant1r  1177  3impdi  1239  vtocl3gf  2974  rspc2ev  3020  reuss  3582  frc  4508  trssord  4558  funtp  5462  resdif  5655  fnotovb  6076  fovrn  6175  fnovrn  6180  fmpt2co  6389  smoord  6586  odi  6781  oeoa  6799  oeoe  6801  nndi  6825  ecopovtrn  6966  ecovass  6975  ecovdi  6976  supmaxlem  7425  suppr  7429  harval2  7840  cdaassen  8018  fin23lem31  8179  tskuni  8614  addasspi  8728  mulasspi  8730  distrpi  8731  mulcanenq  8793  genpass  8842  distrlem1pr  8858  prlem934  8866  ltapr  8878  le2tri3i  9159  subadd  9264  addsub  9272  subdi  9423  submul2  9430  ltaddsub  9458  leaddsub  9460  divval  9636  div12  9656  diveq1  9664  divneg  9665  divdiv2  9682  ltmulgt11  9826  gt0div  9832  ge0div  9833  uzind3  10319  fnn0ind  10325  qdivcl  10551  irrmul  10555  xrlttr  10689  fzen  11028  modcyc  11231  modcyc2  11232  faclbnd4lem4  11542  lenegsq  12079  moddvds  12814  dvdscmulr  12833  dvdsmulcr  12834  dvds2add  12836  dvds2sub  12837  dvdsleabs  12851  divalg  12878  divalgb  12879  ndvdsadd  12883  gcdcllem3  12968  dvdslegcd  12971  modgcd  12991  absmulgcd  13002  odzval  13132  pcmul  13180  ressid2  13472  ressval2  13473  catcisolem  14216  prf1st  14256  prf2nd  14257  1st2ndprf  14258  curfuncf  14290  curf2ndf  14299  pltval  14372  pospo  14385  joinval  14400  joinval2  14401  meetval  14407  meetval2  14408  lubel  14504  isdlat  14574  spwpr4  14618  laspwcl  14621  lanfwcl  14622  mndcl  14650  issubmnd  14679  prdsmndd  14683  submcl  14708  grpinvid1  14808  grpinvid2  14809  mulgp1  14871  ghmlin  14966  ghmsub  14969  odlem2  15132  gexlem2  15171  lsmvalx  15228  efgtval  15310  cmncom  15383  lssvnegcl  15987  islss3  15990  prdslmodd  16000  evlslem2  16523  zntoslem  16792  unopn  16931  ntrss  17074  innei  17144  t1sep2  17387  metustsymOLD  18544  cncfi  18877  evlseu  19890  quotval  20162  abelthlem2  20301  mudivsum  21177  padicabv  21277  grposn  21756  grpoinvid1  21771  grpoinvid2  21772  grpodivval  21784  gxval  21799  ablo4  21828  ablonncan  21835  issubgoi  21851  ablomul  21896  vcnegsubdi2  22007  nvnpcan  22094  nvmeq0  22098  nvabs  22115  imsdval  22131  ipval  22152  nmorepnf  22222  blo3i  22256  blometi  22257  ipasslem5  22289  hvmulcan  22527  his5  22541  his7  22545  his2sub2  22548  hhssnv  22717  fh1  23073  fh2  23074  cm2j  23075  homcl  23202  homco1  23257  homulass  23258  hoadddi  23259  hosubsub2  23268  braadd  23401  bramul  23402  lnopmul  23423  lnopli  23424  lnopaddmuli  23429  lnopsubmuli  23431  lnfnli  23496  lnfnaddmuli  23501  kbass2  23573  mdexchi  23791  xdivval  24118  unitdivcld  24252  cvmlift2lem7  24949  axsegconlem1  25760  finminlem  26211  ivthALT  26228  exidcl  26441  rngoneglmul  26457  rngonegrmul  26458  divrngcl  26463  crngocom  26501  crngm4  26503  inidl  26530  diophren  26764  monotoddzzfi  26895  rpexpmord  26901  ltrmynn0  26903  ltrmxnn0  26904  lermxnn0  26905  rmyeq  26909  lermy  26910  jm2.21  26955  unxpwdom3  27124  dvconstbi  27419  expgrowth  27420  fnotaovb  27929  frgregordn0  28173  onetansqsecsq  28218  bi3impb  28280  eel132  28512  bnj229  28961  bnj546  28973  bnj570  28982  oposlem  29666  hlsuprexch  29863  ldilcnv  30597  ltrnu  30603  tgrpgrplem  31231  tgrpabl  31233  erngdvlem3  31472  erngdvlem3-rN  31480  dvalveclem  31508  dvhfvadd  31574  dvhgrp  31590  dvhlveclem  31591  djhval2  31882
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator