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

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

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1187 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  3anidm23  1278  mp3an2  1303  mpd3an3  1316  rgen3  2919  moi2  3247  sbc3ie  3372  2if2  3948  preq12bg  4162  prel12g  4163  reuhypd  4630  fvtp1g  6040  f1imass  6089  fcof1o  6109  weisoeq  6158  f1ofveu  6198  f1ocnvfv3  6199  curry1f  6779  curry2f  6781  funsssuppss  6828  tfrlem11  6960  oalimcl  7112  oeordsuc  7146  oelim2  7147  nneob  7204  mapxpen  7590  findcard  7665  wemaplem3  7876  en2eqpr  8288  infxpabs  8495  infxp  8498  cfflb  8542  cfsmolem  8553  isf32lem12  8647  fin1a2lem9  8691  fin1a2s  8697  axcc3  8721  axdc3lem4  8736  zornn0g  8788  pwfseqlem4  8943  tskwun  9065  tskint  9066  tskxp  9068  tskmap  9069  gruf  9092  gruwun  9094  grutsk1  9102  addcanpi  9182  ltapi  9186  mul4  9652  add4  9699  2addsub  9738  addsubeq4  9739  muladd  9891  ltleadd  9936  receu  10095  p1le  10286  lemul12b  10300  lbinfm  10397  zdiv  10826  fzind  10854  fnn0ind  10855  uzss  10995  zbtwnre  11065  qmulcl  11085  qreccl  11087  xrlttr  11231  xaddass  11326  xmulasslem3  11363  xmulass  11364  xadddilem  11371  xrsupsslem  11383  xrinfmsslem  11384  supxrunb1  11396  ixxin  11431  ioo0  11439  ico0  11460  ioc0  11461  icc0  11462  iooshf  11488  prunioo  11534  ioojoin  11536  elfz5  11565  elfz0fzfz0  11605  elfzonelfzo  11747  fzind2  11757  mulexpz  12024  expsub  12031  digit2  12117  digit1  12118  facndiv  12184  faclbnd4lem4  12192  faclbnd4  12193  faclbnd5  12194  bccmpl  12205  bcval5  12214  bcpasc  12217  hashunx  12270  swrdspsleq  12463  swrdccat1  12472  swrdccat2  12473  swrdswrd  12475  cats1un  12491  crim  12725  absmax  12938  ello12r  13116  elo12r  13127  climshftlem  13173  2sumeq2dv  13303  expcnv  13447  rpnnen2lem7  13624  dvdsval3  13660  dvdsnegb  13671  muldvds1  13678  muldvds2  13679  dvdscmul  13680  dvdsmulc  13681  dvdsmulcr  13683  dvds2ln  13684  divalgb  13729  ndvdssub  13732  gcddiv  13854  rpexp1i  13928  phiprmpw  13972  pythagtriplem1  14004  pockthg  14088  infpnlem1  14092  4sqlem3  14132  0ramcl  14205  firest  14493  imasaddfnlem  14588  imasleval  14601  xpsfrn2  14630  mrerintcl  14657  iscatd  14733  clatleglb  15418  mreclatBAD  15479  pslem  15498  mrcmndind  15616  grplmulf1o  15722  grplactcnv  15746  mulgnn0subcl  15762  mulgsubcl  15763  mulgdir  15774  issubg2  15818  issubgrpd2  15819  cycsubgcl  15829  cycsubgss  15830  nmzsubg  15844  eqgen  15856  ghmmulg  15881  conjghm  15899  symgfixfo  16067  odeq  16177  odval2  16178  odf1  16187  dfod2  16189  gexdvds  16207  gexdvds2  16208  gexcl2  16212  gexdvds3  16213  sylow2blem2  16244  efgsp1  16358  efgrelexlemb  16371  mulgmhm  16439  mulgghm  16440  iscyggen2  16482  iscyg3  16487  srglmhm  16759  srgrmhm  16760  rnglghm  16819  rngrghm  16820  gsumdixpOLD  16826  gsumdixp  16827  dvdsrcl2  16868  crngunit  16880  kerf1hrm  16957  subrgugrp  17010  cntzsubr  17023  lmodvsdir  17098  lmodvsass  17099  lmodvsghm  17132  lsssubg  17164  lss1d  17170  islbs2  17361  lidlsubg  17423  divscrng  17448  lpigen  17464  xrsdsreval  17986  expghm  18051  expghmOLD  18052  mulgghm2  18053  mulgghm2OLD  18056  ip0r  18194  obs2ss  18282  islindf3  18383  matunit  18619  elcls2  18813  opnnei  18859  innei  18864  iscnp4  19002  cnpnei  19003  iscncl  19008  cnnei  19021  cnconst  19023  ordthauslem  19122  bwth  19148  1stccnp  19201  llyrest  19224  nllyrest  19225  kgenss  19251  xkoccn  19327  kqsat  19439  kqt0lem  19444  isr0  19445  fbssfi  19545  isfild  19566  filcon  19591  trfilss  19597  fgtr  19598  ufileu  19627  ufilen  19638  fmfnfmlem4  19665  fmfnfm  19666  hausflimi  19688  cnpflf2  19708  cnpflf  19709  cnflf  19710  cnpfcf  19749  cnfcf  19750  cnextcn  19774  tmdmulg  19798  clsnsg  19815  tsmsxplem1  19862  tsmsxp  19864  trust  19939  ustuqtop0  19950  ismeti  20035  isxmet2d  20037  elbl2ps  20099  elbl2  20100  xblpnfps  20105  xblpnf  20106  xbln0  20124  blin  20131  blssexps  20136  blssex  20137  blsscls2  20214  blcls  20216  blsscls  20217  metss  20218  metrest  20234  metcn  20253  metustblOLD  20290  metustbl  20291  metutopOLD  20292  psmetutop  20293  nmf2  20320  nmdvr  20386  nmoi  20442  nmoix  20443  nmoleub  20445  nghmcn  20459  xrsxmet  20521  iccntr  20533  metdsle  20563  icoopnst  20646  iocopnst  20647  icccvx  20657  pi1xfr  20762  lmmbr  20904  lmmbr2  20905  iscfil3  20919  iscau2  20923  cfilres  20942  bcthlem1  20970  bcthlem4  20973  bcthlem5  20974  rrxmet  21042  ioombl  21182  iccvolcl  21184  ioovolcl  21186  mbfi1fseqlem3  21331  mbfi1fseqlem4  21332  mbfi1fseqlem5  21333  ig1pcl  21783  ig1prsp  21785  aannenlem1  21930  taylplem1  21964  dvtaylp  21971  relogeftb  22169  logdivlt  22206  cxpexp  22249  rpcxpcl  22257  isppw2  22589  vmappw  22590  lgslem4  22774  lgscllem  22778  lgsneg1  22795  lgsne0  22808  brbtwn2  23323  ax5seglem1  23346  ax5seglem2  23347  axcontlem4  23385  nbgraf1olem5  23526  constr3cycl  23719  grpoidinvlem3  23865  isvci  24132  nmcvcn  24262  ipval2lem2  24271  ipval2lem5  24277  sspival  24308  sspimsval  24310  isblo2  24355  nmoo0  24363  blocni  24377  isph  24394  sspph  24427  hvadd4  24610  hiassdi  24665  ocsh  24858  chj4  25110  spansncol  25143  pjjsi  25275  hoscl  25321  hodcl  25323  hoadd4  25360  homco1  25377  homulass  25378  hoadddi  25379  hoadddir  25380  unoplin  25496  adjvalval  25513  hmoplin  25518  bralnfn  25524  brafnmul  25527  lnopmi  25576  lnopcoi  25579  hmops  25596  hmopm  25597  nmophmi  25607  lnfncnbd  25633  cnlnadjlem2  25644  adjlnop  25662  adjmul  25668  adjadd  25669  branmfn  25681  kbass5  25696  kbass6  25697  leop2  25700  leopadd  25708  leopmuli  25709  pjimai  25752  atcvatlem  25961  chirredlem2  25967  mdsymlem3  25981  mdsymlem5  25983  sumdmdii  25991  sumdmdlem  25994  cdj3lem2a  26012  cdj3lem2b  26013  cdj3lem3a  26015  cdj3i  26017  xreceu  26262  toslublem  26293  tosglblem  26295  xrstos  26305  ogrpaddltbi  26347  archiabllem1a  26373  archiabllem1b  26374  archiabllem2c  26377  archiabl  26380  slmdvsdir  26397  slmdvsass  26398  ordtconlem1  26519  hasheuni  26699  ballotlemirc  27078  signspval  27117  txpcon  27285  cvmscld  27326  2cprodeq2dv  27602  dfrdg2  27773  wsuclem  27926  nobndlem8  28004  segconeu  28206  linecom  28345  linethru  28348  lineintmo  28352  heicant  28594  mblfinlem1  28596  mblfinlem3  28598  ismblfin  28600  cnambfre  28608  itg2addnclem2  28612  ftc1anclem1  28635  ftc1anclem5  28639  ftc1anclem6  28640  ftc2nc  28644  areacirclem2  28653  areacirclem4  28655  areacirclem5  28656  areacirc  28657  fnemeet2  28756  fnejoin2  28758  fzmul  28804  subspopn  28816  isbndx  28849  isbnd2  28850  isbnd3  28851  ssbnd  28855  prdstotbnd  28861  heibor1  28877  rrnmet  28896  rngonegmn1l  28923  rngohomco  28948  rngoisocnv  28955  rngoisoco  28956  crngohomfo  28974  isidlc  28983  rngoidl  28992  prnc  29035  ispridlc  29038  oddcomabszz  29453  acongtr  29489  rpnnen3lem  29548  islssfg  29591  lmhmfgsplit  29607  unxpwdom3  29616  hbtlem7  29649  sdrgacs  29726  hashgcdeq  29734  iocmbl  29756  dvconstbi  29776  otsndisj  30299  ralxfrd2  30305  el2fzo  30380  usg2wlkeq  30457  usgra2pthlem1  30468  wwlknimp  30489  wwlknred  30523  wwlknext  30524  clwwlknprop  30603  3cyclfrgrarn1  30772  3cyclfrgrarn  30773  4cycl2vnunb  30777  frgrancvvdeqlemB  30799  usgreghash2spotv  30827  2spotmdisj  30829  scmatscmids  31046  lcoss  31122  snlindsntorlem  31156  cpmatelimp  31221  cpmatelimp2  31223  cpmatinvcl  31226  cpmatmcl  31228  mat2pmatf  31237  m2cpmf  31251  m2cpmfo  31261  m2cpminv  31268  decpmataa0  31275  pm2mpf  31305  pm2mpf1  31306  idpm2idmp  31308  pm2mpfo  31321  bnj1204  32355  cvrval2  33277  glbconxN  33380  hlrelat5N  33403  cvratlem  33423  cvrat2  33431  athgt  33458  3dim2  33470  llnn0  33518  lplnn0N  33549  lvoln0N  33593  snatpsubN  33752  paddasslem18  33839  pmod1i  33850  lhpexle2  34012  lhpexle3lem  34013  lhpexle3  34014  ldilcnv  34117  trlcnv  34167  trlnidatb  34179  cdleme32snaw  34437  cdleme32fvaw  34441  cdleme42ke  34487  cdlemeg46gf  34535  cdleme50trn12  34554  cdlemg1cex  34590  cdlemb3  34608  tgrpgrplem  34751  tgrpabl  34753  tendoplcl2  34780  tendo0pl  34793  tendoicl  34798  tendoipl  34799  cdlemkid3N  34935  tendoex  34977  erngdvlem4  34993  erngdvlem4-rN  35001  dib1dim  35168  dib1dim2  35171  dihglbcpreN  35303  dihmeetALTN  35330  dih1dimatlem  35332  dihatlat  35337
  Copyright terms: Public domain W3C validator