MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impb Structured version   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  3014  rspc2ev  3060  reuss  3622  frc  4548  trssord  4598  funtp  5503  resdif  5696  fnotovb  6117  fovrn  6216  fnovrn  6221  fmpt2co  6430  smoord  6627  odi  6822  oeoa  6840  oeoe  6842  nndi  6866  ecopovtrn  7007  ecovass  7016  ecovdi  7017  supmaxlem  7469  suppr  7473  harval2  7884  cdaassen  8062  fin23lem31  8223  tskuni  8658  addasspi  8772  mulasspi  8774  distrpi  8775  mulcanenq  8837  genpass  8886  distrlem1pr  8902  prlem934  8910  ltapr  8922  le2tri3i  9203  subadd  9308  addsub  9316  subdi  9467  submul2  9474  ltaddsub  9502  leaddsub  9504  divval  9680  div12  9700  diveq1  9708  divneg  9709  divdiv2  9726  ltmulgt11  9870  gt0div  9876  ge0div  9877  uzind3  10363  fnn0ind  10369  qdivcl  10595  irrmul  10599  xrlttr  10733  fzen  11072  modcyc  11276  modcyc2  11277  faclbnd4lem4  11587  lenegsq  12124  moddvds  12859  dvdscmulr  12878  dvdsmulcr  12879  dvds2add  12881  dvds2sub  12882  dvdsleabs  12896  divalg  12923  divalgb  12924  ndvdsadd  12928  gcdcllem3  13013  dvdslegcd  13016  modgcd  13036  absmulgcd  13047  odzval  13177  pcmul  13225  ressid2  13517  ressval2  13518  catcisolem  14261  prf1st  14301  prf2nd  14302  1st2ndprf  14303  curfuncf  14335  curf2ndf  14344  pltval  14417  pospo  14430  joinval  14445  joinval2  14446  meetval  14452  meetval2  14453  lubel  14549  isdlat  14619  spwpr4  14663  laspwcl  14666  lanfwcl  14667  mndcl  14695  issubmnd  14724  prdsmndd  14728  submcl  14753  grpinvid1  14853  grpinvid2  14854  mulgp1  14916  ghmlin  15011  ghmsub  15014  odlem2  15177  gexlem2  15216  lsmvalx  15273  efgtval  15355  cmncom  15428  lssvnegcl  16032  islss3  16035  prdslmodd  16045  evlslem2  16568  zntoslem  16837  unopn  16976  ntrss  17119  innei  17189  t1sep2  17433  metustsymOLD  18591  cncfi  18924  evlseu  19937  quotval  20209  abelthlem2  20348  mudivsum  21224  padicabv  21324  grposn  21803  grpoinvid1  21818  grpoinvid2  21819  grpodivval  21831  gxval  21846  ablo4  21875  ablonncan  21882  issubgoi  21898  ablomul  21943  vcnegsubdi2  22054  nvnpcan  22141  nvmeq0  22145  nvabs  22162  imsdval  22178  ipval  22199  nmorepnf  22269  blo3i  22303  blometi  22304  ipasslem5  22336  hvmulcan  22574  his5  22588  his7  22592  his2sub2  22595  hhssnv  22764  fh1  23120  fh2  23121  cm2j  23122  homcl  23249  homco1  23304  homulass  23305  hoadddi  23306  hosubsub2  23315  braadd  23448  bramul  23449  lnopmul  23470  lnopli  23471  lnopaddmuli  23476  lnopsubmuli  23478  lnfnli  23543  lnfnaddmuli  23548  kbass2  23620  mdexchi  23838  xdivval  24165  unitdivcld  24299  cvmlift2lem7  24996  axsegconlem1  25856  finminlem  26321  ivthALT  26338  exidcl  26551  rngoneglmul  26567  rngonegrmul  26568  divrngcl  26573  crngocom  26611  crngm4  26613  inidl  26640  diophren  26874  monotoddzzfi  27005  rpexpmord  27011  ltrmynn0  27013  ltrmxnn0  27014  lermxnn0  27015  rmyeq  27019  lermy  27020  jm2.21  27065  unxpwdom3  27233  dvconstbi  27528  expgrowth  27529  fnotaovb  28038  frgregordn0  28459  onetansqsecsq  28504  bi3impb  28566  eel132  28803  bnj229  29255  bnj546  29267  bnj570  29276  oposlem  29981  hlsuprexch  30178  ldilcnv  30912  ltrnu  30918  tgrpgrplem  31546  tgrpabl  31548  erngdvlem3  31787  erngdvlem3-rN  31795  dvalveclem  31823  dvhfvadd  31889  dvhgrp  31905  dvhlveclem  31906  djhval2  32197
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