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

Theorem 3impa 1148
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 588 . 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:  3impdir  1240  syl3an9b  1252  biimp3a  1283  rspec3  2766  rspc3v  3021  raltpg  3819  rextpg  3820  disjiun  4162  opelopabt  4427  ordelinel  4639  3optocl  4913  fun2ssres  5453  funssfv  5705  foco2  5848  f1elima  5968  ot1stg  6320  ot2ndg  6321  smogt  6588  omord2  6769  omword  6772  omass  6782  oeword  6792  nnmass  6826  omabslem  6848  th3q  6972  ecovass  6975  fpmg  6998  f1imaeng  7126  findcard  7306  cdaun  8008  cfsmolem  8106  ingru  8646  addasspi  8728  mulasspi  8730  ltapi  8736  ltmpi  8737  genpass  8842  axpre-ltadd  8998  adddir  9039  leltne  9120  le2tri3i  9159  addsub12  9274  subdir  9424  ltaddsub  9458  leaddsub  9460  recextlem2  9609  div12  9656  divdiv32  9678  divdiv1  9681  lble  9916  fnn0ind  10325  supminf  10519  xrleltne  10694  xrmaxeq  10723  xrmineq  10724  elicc4  10933  iccsplit  10985  elfz  11005  fzrevral  11086  fldiv2  11197  modabs  11229  modsubdir  11240  expgt0  11368  expge0  11371  expge1  11372  mulexpz  11375  expp1z  11383  expm1  11384  digit2  11467  digit1  11468  faclbnd4  11543  faclbnd5  11544  ccatval1  11700  abssubne0  12075  absdiflt  12076  absdifle  12077  binom  12564  cos01gt0  12747  rpnnen2lem4  12772  dvds0lem  12815  dvdsnegb  12822  muldvds1  12829  muldvds2  12830  dvdscmulr  12833  dvdsmulcr  12834  gcdaddm  12984  prmdvdsexp  13069  rpexp1i  13076  monpropd  13918  prfval  14251  xpcpropd  14260  curf2ndf  14299  lubub  14501  lubl  14502  eqglact  14946  mndodcongi  15136  oddvdsnn0  15137  efgi0  15307  efgi1  15308  lss0cl  15978  ipcl  16819  opnneiss  17137  cnpval  17254  cnf2  17267  cnnei  17300  llyi  17490  nllyi  17491  ptpjcn  17596  cnmptk2  17671  flfval  17975  cnmpt2plusg  18071  cnmpt2vsca  18177  ustincl  18190  xbln0  18397  blssec  18418  blpnfctr  18419  mopni2  18476  mopni3  18477  nmoval  18702  nmocl  18707  isnghm2  18711  isnmhm2  18739  cnmpt2ds  18827  metdseq0  18837  cnmpt2ip  19155  caucfil  19189  mbfimasn  19479  dvnf  19766  dvnbss  19767  coemul  20123  dvply1  20154  dvnply2  20157  pserdvlem2  20297  logeftb  20431  advlogexp  20499  cxpne0  20521  cxpp1  20524  logrec  20614  lgsne0  21070  umgrass  21307  umgran0  21308  umgrale  21309  nbgraf1olem3  21406  pthdepisspth  21527  grposn  21756  issubgoi  21851  ablomul  21896  sspval  22175  sspnval  22189  lnof  22209  lnocoi  22211  nmooval  22217  nmooge0  22221  nmoub3i  22227  bloln  22238  nmblore  22240  hvaddsubass  22496  hvmulcan2  22528  hhssnv  22717  hosval  23196  homval  23197  hodval  23198  hfsval  23199  hfmval  23200  homco1  23257  homulass  23258  hoadddir  23260  hoaddsubass  23271  hosubsub4  23274  nmopub2tALT  23365  nmfnleub2  23382  kbval  23410  lnopmul  23423  lnopmulsubi  23432  0lnfn  23441  lnopcoi  23459  nmcoplb  23486  nmcfnlb  23510  kbass2  23573  nmopleid  23595  hstoh  23688  mdi  23751  dmdi  23758  dmdi4  23763  mdsl3  23772  cdj3lem2  23891  supxrnemnf  24080  iccgelb  24089  dedekind  25140  elno2  25522  ax5seglem9  25780  fnessex  26245  fzmul  26334  incsequz2  26343  nninfnub  26345  exidreslem  26442  ghomf  26447  rngohomf  26472  rngohom1  26474  rngohomadd  26475  rngohommul  26476  rngoiso1o  26485  rngoisohom  26486  igenmin  26564  3anrabdioph  26731  3orrabdioph  26732  rencldnfilem  26771  expmordi  26900  divalgmodcl  26948  jm2.18  26949  jm2.25  26960  jm2.15nn0  26964  addrfv  27541  subrfv  27542  mulvfv  27543  stoweidlem34  27650  stoweidlem48  27664  aovmpt4g  27932  bi3impa  28281  bnj563  28817  bnj605  28984  bnj607  28993  bnj1097  29056  lkrcl  29575  lkrf0  29576  omlfh1N  29741  tendoex  31457
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