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

Theorem 3impa 1202
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3impa  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 608 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1201 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  3impdir  1323  syl3an9b  1336  biimp3a  1368  stoic3  1659  rspec3  2760  rspc3v  3161  raltpg  4022  rextpg  4023  disjiun  4392  3optocl  4912  fun2ssres  5622  funssfv  5878  foco2  6040  f1elima  6162  ot1stg  6804  ot2ndg  6805  smogt  7083  omord2  7265  omword  7268  oeword  7288  omabslem  7344  ecovass  7467  fpmg  7494  findcard  7807  cdaun  8599  cfsmolem  8697  ingru  9237  addasspi  9317  mulasspi  9319  ltapi  9325  ltmpi  9326  axpre-ltadd  9588  leltne  9720  dedekind  9794  recextlem2  10240  divdiv32  10312  divdiv1  10315  lble  10555  fnn0ind  11031  supminf  11247  supminfOLD  11248  xrleltne  11441  xrmaxeq  11471  xrmineq  11472  iccgelb  11688  elicc4  11698  iccsplit  11762  elfz  11787  fzrevral  11876  modabs  12127  expgt0  12302  expge0  12305  expge1  12306  mulexpz  12309  expp1z  12318  expm1  12319  digit1  12403  faclbnd4  12479  faclbnd5  12480  abssubne0  13372  binom  13881  dvds0lem  14306  dvdsnegb  14313  muldvds1  14320  muldvds2  14321  dvdscmulr  14324  dvdsmulcr  14325  gcdaddm  14486  lcmdvds  14566  prmdvdsexp  14660  rpexp1i  14666  monpropd  15635  prfval  16077  xpcpropd  16086  curf2ndf  16125  eqglact  16861  mndodcongi  17185  oddvdsnn0  17186  efgi0  17363  efgi1  17364  lss0cl  18163  scmatscmid  19524  pmatcollpw3fi1lem1  19803  cnpval  20245  cnf2  20258  cnnei  20291  lfinun  20533  ptpjcn  20619  cnmptk2  20694  flfval  20998  cnmpt2plusg  21096  cnmpt2vsca  21202  ustincl  21215  xbln0  21422  blssec  21443  blpnfctr  21444  mopni2  21501  mopni3  21502  nmoval  21713  nmocl  21718  isnghm2  21722  nmovalOLD  21732  nmoclOLD  21736  isnghm2OLD  21740  isnmhm2  21766  cnmpt2ds  21854  metdseq0  21864  metdseq0OLD  21879  cnmpt2ip  22212  caucfil  22246  mbfimasn  22583  dvnf  22874  dvnbss  22875  coemul  23199  dvply1  23230  dvnply2  23233  pserdvlem2  23376  logeftb  23526  advlogexp  23593  cxpne0  23615  cxpp1  23618  lgsne0  24254  f1otrg  24894  ax5seglem9  24960  umgrass  25039  umgran0  25040  umgrale  25041  nbgraf1olem3  25164  pthdepisspth  25297  grposn  25936  sspval  26355  sspnval  26369  lnof  26389  nmooval  26397  nmooge0  26401  nmoub3i  26407  bloln  26418  nmblore  26420  hosval  27386  homval  27387  hodval  27388  hfsval  27389  hfmval  27390  homulass  27448  hoadddir  27450  nmopub2tALT  27555  nmfnleub2  27572  kbval  27600  lnopmul  27613  0lnfn  27631  lnopcoi  27649  nmcoplb  27676  nmcfnlb  27700  kbass2  27763  nmopleid  27785  hstoh  27878  mdi  27941  dmdi  27948  dmdi4  27953  supxrnemnf  28347  reofld  28596  bnj605  29711  bnj607  29720  bnj1097  29783  elno2  30534  topdifinffinlem  31743  ftc1anclem2  32011  fzmul  32062  nninfnub  32073  exidreslem  32168  ghomf  32173  rngohomf  32198  rngohom1  32200  rngohomadd  32201  rngohommul  32202  rngoiso1o  32211  rngoisohom  32212  igenmin  32290  lkrcl  32652  lkrf0  32653  omlfh1N  32818  tendoex  34536  3anrabdioph  35619  3orrabdioph  35620  rencldnfilem  35657  expmordi  35789  dvdsabsmod0  35834  divalgmodcl  35836  jm2.18  35837  jm2.25  35848  jm2.15nn0  35852  addrfv  36816  subrfv  36817  mulvfv  36818  bi3impa  36834  ex3  36931  ssfiunibd  37521  dvnmul  37812  stoweidlem34  37889  stoweidlem48  37903  sge0cl  38217  sge0xp  38265  ovnsubaddlem1  38386  aovmpt4g  38697  gboage9  38859  uhgrn0  39144  upgrn0  39167  upgrle  39168
  Copyright terms: Public domain W3C validator