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

Theorem 3impa 1200
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 607 . 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:  3impdir  1320  syl3an9b  1333  biimp3a  1364  stoic3  1656  rspec3  2796  rspc3v  3191  raltpg  4045  rextpg  4046  disjiun  4408  3optocl  4924  fun2ssres  5633  funssfv  5887  foco2  6048  f1elima  6170  ot1stg  6812  ot2ndg  6813  smogt  7085  omord2  7267  omword  7270  oeword  7290  omabslem  7346  ecovass  7469  fpmg  7496  findcard  7807  cdaun  8591  cfsmolem  8689  ingru  9229  addasspi  9309  mulasspi  9311  ltapi  9317  ltmpi  9318  axpre-ltadd  9580  leltne  9712  dedekind  9786  recextlem2  10232  divdiv32  10304  divdiv1  10307  lble  10547  fnn0ind  11023  supminf  11239  supminfOLD  11240  xrleltne  11433  xrmaxeq  11463  xrmineq  11464  iccgelb  11680  elicc4  11690  iccsplit  11752  elfz  11777  fzrevral  11866  modabs  12116  expgt0  12291  expge0  12294  expge1  12295  mulexpz  12298  expp1z  12307  expm1  12308  digit1  12392  faclbnd4  12468  faclbnd5  12469  abssubne0  13347  binom  13855  dvds0lem  14280  dvdsnegb  14287  muldvds1  14294  muldvds2  14295  dvdscmulr  14298  dvdsmulcr  14299  gcdaddm  14456  lcmdvds  14533  prmdvdsexp  14627  rpexp1i  14633  monpropd  15586  prfval  16028  xpcpropd  16037  curf2ndf  16076  eqglact  16812  mndodcongi  17127  oddvdsnn0  17128  efgi0  17298  efgi1  17299  lss0cl  18098  scmatscmid  19455  pmatcollpw3fi1lem1  19734  cnpval  20176  cnf2  20189  cnnei  20222  lfinun  20464  ptpjcn  20550  cnmptk2  20625  flfval  20929  cnmpt2plusg  21027  cnmpt2vsca  21133  ustincl  21146  xbln0  21353  blssec  21374  blpnfctr  21375  mopni2  21432  mopni3  21433  nmoval  21640  nmocl  21645  isnghm2  21649  isnmhm2  21677  cnmpt2ds  21765  metdseq0  21775  cnmpt2ip  22105  caucfil  22139  mbfimasn  22464  dvnf  22755  dvnbss  22756  coemul  23071  dvply1  23102  dvnply2  23105  pserdvlem2  23245  logeftb  23395  advlogexp  23462  cxpne0  23484  cxpp1  23487  lgsne0  24121  f1otrg  24744  ax5seglem9  24810  umgrass  24889  umgran0  24890  umgrale  24891  nbgraf1olem3  25013  pthdepisspth  25146  grposn  25785  sspval  26204  sspnval  26218  lnof  26238  nmooval  26246  nmooge0  26250  nmoub3i  26256  bloln  26267  nmblore  26269  hosval  27225  homval  27226  hodval  27227  hfsval  27228  hfmval  27229  homulass  27287  hoadddir  27289  nmopub2tALT  27394  nmfnleub2  27411  kbval  27439  lnopmul  27452  0lnfn  27470  lnopcoi  27488  nmcoplb  27515  nmcfnlb  27539  kbass2  27602  nmopleid  27624  hstoh  27717  mdi  27780  dmdi  27787  dmdi4  27792  supxrnemnf  28187  reofld  28439  bnj605  29503  bnj607  29512  bnj1097  29575  elno2  30325  topdifinffinlem  31481  ftc1anclem2  31722  fzmul  31773  nninfnub  31784  exidreslem  31879  ghomf  31884  rngohomf  31909  rngohom1  31911  rngohomadd  31912  rngohommul  31913  rngoiso1o  31922  rngoisohom  31923  igenmin  32001  lkrcl  32367  lkrf0  32368  omlfh1N  32533  tendoex  34251  3anrabdioph  35334  3orrabdioph  35335  rencldnfilem  35372  expmordi  35505  dvdsabsmod0  35550  divalgmodcl  35552  jm2.18  35553  jm2.25  35564  jm2.15nn0  35568  addrfv  36463  subrfv  36464  mulvfv  36465  bi3impa  36481  ex3  36579  ssfiunibd  37140  dvnmul  37391  stoweidlem34  37468  stoweidlem48  37482  sge0cl  37761  aovmpt4g  38106  gboage9  38268
  Copyright terms: Public domain W3C validator