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

Theorem 3expia 1155
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expia  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mp3an3  1268  3gencl  2978  moi  3109  disji  4192  reusv6OLD  4725  nnsuc  4853  3optocl  4945  sossfld  5308  soisores  6038  isomin  6048  isofrlem  6051  ovmpt2s  6188  ov2gf  6189  ndmovord  6228  poxp  6449  brtpos  6479  dfsmo2  6600  smoiun  6614  smoord  6618  smogt  6620  omeulem1  6816  omeu  6819  oewordi  6825  uniinqs  6975  mapvalg  7019  pmvalg  7020  elmapg  7022  xpdom3  7197  mapdom3  7270  php3  7284  unxpdomlem3  7306  isinf  7313  findcard2  7339  isfinite2  7356  ordiso  7474  cnfcom3clem  7651  r111  7690  tskwe  7826  pr2ne  7878  infxpenlem  7884  dfac8alem  7899  infdif  8078  infdif2  8079  cff1  8127  coflim  8130  cfslbn  8136  cfslb2n  8137  cofsmo  8138  cfsmolem  8139  cfcoflem  8141  fin23lem27  8197  isf32lem9  8230  isf34lem6  8249  axcc2lem  8305  domtriomlem  8311  axdc4lem  8324  zorn2lem2  8366  axdclem2  8389  konigthlem  8432  gchen1  8489  gchen2  8490  gchpwdom  8538  gchaleph  8539  winainflem  8557  tskcard  8645  gruiun  8663  gruen  8676  intgru  8678  grudomon  8681  grur1a  8683  grutsk1  8685  nqereu  8795  nqereq  8801  ltsonq  8835  prlem934  8899  reclem3pr  8915  1re  9079  axsup  9140  ltlen  9164  addid2  9238  recex  9643  lemul1a  9853  ledivmulOLD  9873  lt2msq  9883  fimaxre2  9945  zdiv  10329  zextlt  10333  prime  10339  uzind2  10351  fzind  10357  lbzbi  10553  qbtwnxr  10775  qextltlem  10777  xralrple  10780  xltneg  10792  xlt2add  10828  supxrgtmnf  10897  ixxub  10926  ixxlb  10927  ioo0  10930  ico0  10951  ioc0  10952  icc0  10953  iocssre  10979  icossre  10980  iccssre  10981  fzen  11061  expclzlem  11393  expaddz  11412  expmulz  11414  hashgadd  11639  ccatopth2  11765  shftuz  11872  cau3lem  12146  caubnd  12150  climuni  12334  lo1resb  12346  o1resb  12348  o1of2  12394  o1add  12395  o1mul  12396  o1sub  12397  eflt  12706  znnenlem  12799  moddvds  12847  dvdscmulr  12866  dvdsmulcr  12867  dvdsle  12883  divalglem8  12908  divalgb  12912  ndvdssub  12915  bitsfzo  12935  gcdcllem1  12999  gcdcllem3  13001  dvdsgcd  13031  isprm3  13076  coprm  13088  qredeu  13095  prmdvdsexpr  13104  prmexpb  13105  eulerthlem2  13159  fermltl  13161  coprimeprodsq  13171  pythagtrip  13196  pcprendvds  13202  pcpremul  13205  pcdvdsb  13230  pc2dvds  13240  4sqlem12  13312  4sqlem18  13318  vdwlem10  13346  xpslem  13786  ismred  13815  mrieqv2d  13852  iscatd  13886  isfuncd  14050  poslubd  14562  dirtr  14669  ghmrn  15007  mndodcongi  15169  oddvdsnn0  15170  oddvds  15173  odcl2  15189  odhash3  15198  gexdvds  15206  pgpfi  15227  lsmss1b  15287  lsmss2b  15289  efgsrel  15354  efgred  15368  cntzcmn  15447  cyggenod  15482  lt6abl  15492  gsumcom2  15537  pgpfac1lem2  15621  pgpfac1lem3  15623  dvdsunit  15756  unitmulclb  15758  irredrmul  15800  isabvd  15896  lmodvsdi  15961  lss0cl  16011  islbs3  16215  lbsextlem2  16219  mvrf1  16477  xrsdsreclblem  16732  opnnei  17172  neindisj2  17175  cncls2  17325  cncls  17326  cnntr  17327  cnpresti  17340  cnprest  17341  lmcnp  17356  isreg2  17429  ordthauslem  17435  uncon  17480  2ndc1stc  17502  kgen2ss  17575  ptclsg  17635  cnmptcom  17698  kqfvima  17750  hmeof1o  17784  fbncp  17859  fbfinnfr  17861  trfbas2  17863  isufil2  17928  ufprim  17929  trufil  17930  filufint  17940  hausflim  18001  flimrest  18003  flimcls  18005  cnpfcf  18061  alexsubALT  18070  tmdgsum  18113  opnsubg  18125  cldsubg  18128  divstgpopn  18137  tsmsxp  18172  blpnf  18415  blssps  18442  blss  18443  blssec  18453  neibl  18519  prdsxmslem2  18547  xrsmopn  18831  metnrm  18880  climcncf  18918  iccpnfhmeo  18958  xrhmeo  18959  bndth  18971  cphsqrcl3  19138  iscau2  19218  iscmet3lem2  19233  bcthlem5  19269  bcth3  19272  ishl2  19312  ivthlem1  19336  cmmbl  19417  iundisj2  19431  voliunlem2  19433  mbfaddlem  19540  itg2itg1  19616  itg2seq  19622  itg2mulclem  19626  cnplimc  19762  dvres2  19787  deg1nn0clb  20001  deg1lt0  20002  deg1ge  20009  plypf1  20119  plyadd  20124  plymul  20125  coeeu  20132  dgrub2  20142  coeidlem  20144  coeid3  20147  coemullem  20156  coe11  20159  coemulhi  20160  coemulc  20161  dgreq0  20171  dgrlt  20172  dgradd2  20174  vieta1lem2  20216  sineq0  20417  tanord1  20427  tanord  20428  cxpeq0  20557  cxpmul2z  20570  cxpcn3lem  20619  angpieqvd  20660  o1cxp  20801  scvxcvx  20812  chtublem  20983  bposlem3  21058  lgsqr  21118  dchrisumlema  21170  dchrisumlem2  21172  ostth2lem3  21317  sizeusglecusg  21483  lpni  21755  gxnn0neg  21839  gxnn0suc  21840  gxcl  21841  gxneg  21842  gxcom  21845  gxinv  21846  gxsuc  21848  gxnn0add  21850  gxadd  21851  gxnn0mul  21853  gxmul  21854  ipasslem5  22324  htthlem  22408  omlsii  22893  spansni  23047  spansneleq  23060  elspansn4  23063  sumspansn  23139  homco1  23292  homulass  23293  mdsl0  23801  ssdmd1  23804  ssdmd2  23805  cvdmd  23828  chirredlem2  23882  atdmd  23889  atmd2  23891  disjif  24008  iundisj2f  24018  isoun  24077  iocinioc2  24130  iundisj2fi  24141  logccne0  24384  indpi1  24407  measinblem  24562  measres  24564  measdivcstOLD  24566  mbfmco2  24603  orvclteinc  24721  cvmlift2lem10  24987  ghomf1olem  25093  ntrivcvgmul  25219  nodense  25598  dfrdg4  25745  brbtwn2  25792  axpasch  25828  axcontlem4  25854  axcontlem5  25855  brcolinear2  25940  brsegle2  25991  limsucncmpi  26143  ee7.2aOLD  26159  areacirc  26234  nn0prpw  26263  ntruni  26267  clsint2  26269  fnessref  26310  fnemeet2  26333  fnejoin2  26335  filbcmb  26379  mettrifi  26400  heiborlem8  26464  heiborlem10  26466  heibor  26467  riscer  26541  igenval2  26613  oddcomabszz  26944  jm2.19lem4  27000  fiuneneq  27428  idomsubgmo  27429  addrcom  27594  stoweidlem26  27689  stoweidlem34  27697  swrdccatin12lem3c  28098  swrdccatin12lem3  28099  shwrdssizelem4  28170  int3  28567  suctrALTcf  28888  suctrALT3  28890  chordthmALT  28900  iunconlem2  28902  bnj605  29132  bnj607  29141  bnj964  29168  bnj1033  29192  bnj1128  29213  bnj1137  29218  bnj1136  29220  bnj1413  29258  bnj60  29285  lshpcmp  29625  eqlkr  29736  lkrlsp2  29740  lkrshp  29742  cvrnbtwn2  29912  cvlexch3  29969  cvlexch4N  29970  cvlatexchb1  29971  cvlsupr3  29981  exatleN  30040  cvratlem  30057  atcvrj2b  30068  cvrat3  30078  cvrat4  30079  athgt  30092  ps-1  30113  ps-2  30114  3atlem5  30123  3at  30126  llnneat  30150  llnmlplnN  30175  lplnneat  30181  lplnnelln  30182  islpln2a  30184  lplnriaN  30186  lplnribN  30187  lplnexllnN  30200  2llnjaN  30202  lvolnle3at  30218  lvolneatN  30224  lvolnelln  30225  lvolnelpln  30226  islvol2aN  30228  dalem62  30370  pmapglb2N  30407  pmapglb2xN  30408  lncmp  30419  paddasslem14  30469  paddasslem15  30470  pmod2iN  30485  hlmod1i  30492  pclfinclN  30586  osumcllem8N  30599  pexmidlem4N  30609  pl42lem1N  30615  pl42lem4N  30618  lhpexle1  30644  lhpexle2lem  30645  lhpmcvr5N  30663  lhpmcvr6N  30664  ltrneq  30785  trlnidatb  30813  cdleme0ex2N  30860  cdleme27a  31003  cdleme17d3  31132  cdlemeg46gfre  31168  cdleme48gfv1  31172  cdlemeg49lebilem  31175  cdlemf2  31198  cdlemf  31199  cdlemfnid  31200  trlord  31205  cdlemg31c  31335  cdlemg35  31349  trlcone  31364  tendoeq2  31410  cdlemj3  31459  cdlemk26b-3  31541  cdlemk33N  31545  cdleml3N  31614  cdlemn  31849  dih1dimb2  31878  dihord5apre  31899  dihmeetlem1N  31927  dihglblem5apreN  31928  dihglblem2N  31931  dihglblem3N  31932  dihmeetlem13N  31956  dihmeetlem15N  31958  dihatexv  31975  hdmap14lem12  32519
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