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

Theorem 3impb 1201
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 608 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3adant1l  1256  3adant1r  1257  3impdi  1319  rsp2e  2891  vtocl3gf  3148  rspc2ev  3199  reuss  3760  frc  4820  trssord  5459  funtp  5653  resdif  5851  fnotovb  6346  fovrn  6453  fnovrn  6458  fmpt2co  6890  smoord  7092  odi  7288  oeoa  7306  oeoe  7308  nndi  7332  ecopovtrn  7474  ecovass  7478  ecovdi  7479  supmaxlemOLD  7988  suppr  7993  infpr  8019  harval2  8430  cdaassen  8610  fin23lem31  8771  tskuni  9207  addasspi  9319  mulasspi  9321  distrpi  9322  mulcanenq  9384  genpass  9433  distrlem1pr  9449  prlem934  9457  ltapr  9469  le2tri3i  9763  subadd  9877  addsub  9885  subdi  10051  submul2  10058  ltaddsub  10087  leaddsub  10089  divval  10271  div12  10291  diveq1  10300  divneg  10301  divdiv2  10318  ltmulgt11  10464  gt0div  10470  ge0div  10471  uzind3  11029  fnn0ind  11034  qdivcl  11285  irrmul  11289  xrlttr  11439  fzen  11814  modcyc  12129  modcyc2  12130  faclbnd4lem4  12478  cshweqdifid  12904  lenegsq  13362  moddvds  14290  dvdscmulr  14309  dvdsmulcr  14310  dvds2add  14312  dvds2sub  14313  dvdsleabs  14329  divalg  14359  divalgb  14360  ndvdsadd  14364  gcdcllem3  14449  dvdslegcd  14452  modgcd  14474  absmulgcd  14486  odzval  14705  pcmul  14764  ressid2  15139  ressval2  15140  catcisolem  15952  prf1st  16040  prf2nd  16041  1st2ndprf  16042  curfuncf  16074  curf2ndf  16083  pltval  16157  pospo  16170  lubel  16319  isdlat  16390  issubmnd  16515  prdsmndd  16520  submcl  16551  grpinvid1  16665  grpinvid2  16666  mulgp1  16735  ghmlin  16839  ghmsub  16842  odlem2  17130  gexlem2  17169  lsmvalx  17226  efgtval  17308  cmncom  17381  lssvnegcl  18114  islss3  18117  prdslmodd  18127  evlslem2  18670  evlseu  18674  zntoslem  19058  maducoeval2  19596  madutpos  19598  madugsum  19599  madurid  19600  m2cpminvid  19708  pm2mpghm  19771  unopn  19864  ntrss  20001  innei  20072  t1sep2  20316  metustsym  21501  cncfi  21822  rrxds  22245  quotval  23113  abelthlem2  23252  mudivsum  24231  padicabv  24331  axsegconlem1  24793  frgregordn0  25643  grposn  25788  grpoinvid1  25803  grpoinvid2  25804  grpodivval  25816  gxval  25831  ablo4  25860  ablonncan  25867  issubgoi  25883  ablomul  25928  vcnegsubdi2  26039  nvnpcan  26126  nvmeq0  26130  nvabs  26147  imsdval  26163  ipval  26184  nmorepnf  26254  blo3i  26288  blometi  26289  ipasslem5  26321  hvmulcan  26560  his5  26574  his7  26578  his2sub2  26581  hhssnv  26750  fh1  27106  fh2  27107  cm2j  27108  homcl  27234  homco1  27289  homulass  27290  hoadddi  27291  hosubsub2  27300  braadd  27433  bramul  27434  lnopmul  27455  lnopli  27456  lnopaddmuli  27461  lnopsubmuli  27463  lnfnli  27528  lnfnaddmuli  27533  kbass2  27605  mdexchi  27823  xdivval  28226  resvid2  28430  resvval2  28431  unitdivcld  28546  bnj229  29483  bnj546  29495  bnj570  29504  cvmlift2lem7  29820  finminlem  30759  ivthALT  30776  topdifinffinlem  31484  exidcl  31878  rngoneglmul  31894  rngonegrmul  31895  divrngcl  31900  crngocom  31938  crngm4  31940  inidl  31967  oposlem  32457  hlsuprexch  32655  ldilcnv  33389  ltrnu  33395  tgrpgrplem  34025  tgrpabl  34027  erngdvlem3  34266  erngdvlem3-rN  34274  dvalveclem  34302  dvhfvadd  34368  dvhgrp  34384  dvhlveclem  34385  djhval2  34676  diophren  35365  monotoddzzfi  35496  rpexpmord  35502  ltrmynn0  35504  ltrmxnn0  35505  lermxnn0  35506  rmyeq  35510  lermy  35511  jm2.21  35555  radcnvrat  36300  dvconstbi  36320  expgrowth  36321  bi3impb  36476  eel132  36719  fnotaovb  38090  ccatpfx  38340  submgmcl  38552  onetansqsecsq  39242
  Copyright terms: Public domain W3C validator