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

Theorem 3expia 1233
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 1230 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 436 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  mp3an3  1379  3gencl  3065  moi  3209  disji  4383  3optocl  4918  sossfld  5289  f1oresrab  6071  soisores  6236  isomin  6246  isofrlem  6249  ovmpt2s  6439  ov2gf  6440  ndmovord  6478  nnsuc  6728  poxp  6927  brtpos  7000  dfsmo2  7084  smoiun  7098  smoord  7102  smogt  7104  omeulem1  7301  omeu  7304  oewordi  7310  uniinqs  7461  mapvalg  7500  pmvalg  7501  elmapg  7503  xpdom3  7688  mapdom3  7762  php3  7776  unxpdomlem3  7796  isinf  7803  findcard2  7829  isfinite2  7847  ordiso  8049  cnfcom3clem  8228  r111  8264  tskwe  8402  pr2ne  8454  infxpenlem  8462  dfac8alem  8478  infdif  8657  infdif2  8658  cff1  8706  coflim  8709  cfslbn  8715  cfslb2n  8716  cofsmo  8717  cfsmolem  8718  cfcoflem  8720  fin23lem27  8776  isf32lem9  8809  isf34lem6  8828  axcc2lem  8884  domtriomlem  8890  axdc4lem  8903  zorn2lem2  8945  axdclem2  8968  konigthlem  9011  gchen1  9068  gchen2  9069  gchpwdom  9113  gchaleph  9114  winainflem  9136  tskcard  9224  gruiun  9242  gruen  9255  intgru  9257  grudomon  9260  grur1a  9262  grutsk1  9264  nqereu  9372  nqereq  9378  ltsonq  9412  prlem934  9476  reclem3pr  9492  1re  9660  axsup  9727  ltlen  9753  addid2  9834  recex  10266  lemul1a  10481  lt2msq  10513  fimaxre2  10574  zdiv  11029  zextlt  11033  prime  11039  uzind2  11051  fzind  11056  lbzbi  11275  qbtwnxr  11516  qextltlem  11518  xralrple  11521  xltneg  11533  xlt2add  11571  supxrgtmnf  11640  ixxub  11681  ixxlb  11682  ixxlbOLD  11683  ioo0  11686  ico0  11707  ioc0  11708  icc0  11709  iocssre  11739  icossre  11740  iccssre  11741  fzen  11842  expclzlem  12334  expaddz  12354  expmulz  12356  hashgadd  12594  elovmpt2wrd  12760  ccatopth2  12881  cshf1  12966  shftuz  13209  cau3lem  13494  caubnd  13498  climuni  13693  lo1resb  13705  o1resb  13707  o1of2  13753  o1add  13754  o1mul  13755  o1sub  13756  ntrivcvgmul  14035  eflt  14248  znnenlem  14341  moddvds  14389  dvdscmulr  14408  dvdsmulcr  14409  dvdsle  14427  divalglem8  14459  divalgb  14464  ndvdssub  14467  bitsfzo  14488  gcdcllem1  14552  gcdcllem3  14554  dvdsgcd  14590  lcmgcdlem  14650  lcmfeq0b  14682  isprm3  14712  coprm  14736  qredeu  14743  prmdvdsexpr  14748  prmexpb  14749  eulerthlem2  14809  fermltl  14811  coprimeprodsq  14838  pythagtrip  14863  pcprendvds  14869  pcpremul  14872  pcdvdsb  14897  pc2dvds  14907  4sqlem12  14979  4sqlem18OLD  14985  4sqlem18  14991  vdwlem10  15019  cshwshashlem3  15146  xpslem  15557  ismred  15586  mrieqv2d  15623  iscatd  15657  isfuncd  15848  fthestrcsetc  16113  fthsetcestrc  16128  poslubd  16472  dirtr  16560  ghmrn  16974  pmtrprfv3  17173  mndodcongi  17270  oddvdsnn0  17271  oddvds  17274  odcl2  17294  odhash3  17303  gexdvds  17313  pgpfi  17335  lsmss1b  17395  lsmss2b  17397  efgsrel  17462  efgred  17476  cntzcmn  17558  cyggenod  17597  lt6abl  17607  gsumcom2  17685  pgpfac1lem2  17786  pgpfac1lem3  17788  dvdsunit  17969  unitmulclb  17971  irredrmul  18013  isabvd  18126  lmodvsdi  18192  lss0cl  18248  islbs3  18456  lbsextlem2  18460  mvrf1  18726  coe1fzgsumd  18973  gsummoncoe1  18975  evl1gsumd  19022  xrsdsreclblem  19091  scmataddcl  19618  scmatsubcl  19619  mdetunilem9  19722  mdetuni0  19723  mdetmul  19725  m2cpmrngiso  19859  pm2mpf1  19900  opnnei  20213  neindisj2  20216  cncls2  20366  cncls  20367  cnntr  20368  cnpresti  20381  cnprest  20382  lmcnp  20397  isreg2  20470  ordthauslem  20476  uncon  20521  2ndc1stc  20543  kgen2ss  20647  ptclsg  20707  cnmptcom  20770  kqfvima  20822  hmeof1o  20856  fbncp  20932  fbfinnfr  20934  trfbas2  20936  isufil2  21001  ufprim  21002  trufil  21003  filufint  21013  hausflim  21074  flimrest  21076  flimcls  21078  cnpfcf  21134  alexsubALT  21144  tmdgsum  21188  opnsubg  21200  cldsubg  21203  qustgpopn  21212  tsmsxp  21247  blpnf  21490  blssps  21517  blss  21518  blssec  21528  neibl  21594  prdsxmslem2  21622  xrsmopn  21908  metnrm  21972  climcncf  22010  iccpnfhmeo  22051  xrhmeo  22052  bndth  22064  cphsqrtcl3  22243  iscau2  22325  iscmet3lem2  22340  bcthlem5  22374  bcth3  22377  ishl2  22415  ivthlem1  22480  cmmbl  22566  iundisj2  22581  voliunlem2  22583  mbfaddlem  22695  itg2itg1  22773  itg2seq  22779  itg2mulclem  22783  cnplimc  22921  dvres2  22946  deg1nn0clb  23118  deg1lt0  23119  deg1ge  23126  plypf1  23245  plyadd  23250  plymul  23251  coeeu  23258  dgrub2  23268  coeidlem  23270  coeid3  23273  coemullem  23283  coe11  23286  coemulhi  23287  coemulc  23288  dgreq0  23298  dgrlt  23299  dgradd2  23301  vieta1lem2  23343  sineq0  23555  tanord1  23565  tanord  23566  logccne0  23607  cxpeq0  23702  cxpmul2z  23715  cxpcn3lem  23766  relogbzcl  23790  angpieqvd  23836  o1cxp  23979  scvxcvx  23990  chtublem  24218  bposlem3  24293  lgsqr  24353  dchrisumlema  24405  dchrisumlem2  24407  ostth2lem3  24552  iscgrglt  24638  tghilberti2  24762  inagswap  24959  f1otrg  24980  brbtwn2  25014  axpasch  25050  axcontlem4  25076  axcontlem5  25077  sizeusglecusg  25293  wwlkextproplem3  25550  lpni  25990  gxnn0neg  26072  gxnn0suc  26073  gxcl  26074  gxneg  26075  gxcom  26078  gxinv  26079  gxsuc  26081  gxnn0add  26083  gxadd  26084  gxnn0mul  26086  gxmul  26087  ipasslem5  26557  htthlem  26651  omlsii  27137  spansni  27291  spansneleq  27304  elspansn4  27307  sumspansn  27383  homco1  27535  homulass  27536  mdsl0  28044  ssdmd1  28047  ssdmd2  28048  cvdmd  28071  chirredlem2  28125  atdmd  28132  atmd2  28134  disjif  28265  iundisj2f  28277  isoun  28357  padct  28382  iocinioc2  28436  iundisj2fi  28448  archiabllem1a  28582  archiabllem2a  28585  slmdvsdi  28605  ordtconlem1  28804  indpi1  28917  measinblem  29116  measres  29118  measdivcstOLD  29120  mbfmco2  29160  orvclteinc  29381  sgn3da  29485  sgnnbi  29489  sgnpbi  29490  bnj605  29790  bnj607  29799  bnj964  29826  bnj1033  29850  bnj1128  29871  bnj1137  29876  bnj1136  29878  bnj1413  29916  bnj60  29943  cvmlift2lem10  30107  msubvrs  30270  ghomf1olem  30384  wsuclem  30579  nosepon  30627  nodense  30649  dfrdg4  30789  brcolinear2  30896  brsegle2  30947  nn0prpw  31050  ntruni  31054  clsint2  31056  fnessref  31084  fnemeet2  31094  fnejoin2  31096  limsucncmpi  31176  ee7.2aOLD  31192  dissneqlem  31812  isbasisrelowllem1  31828  isbasisrelowllem2  31829  icoreclin  31830  poimirlem9  32013  poimirlem30  32034  poimirlem32  32036  areacirc  32101  filbcmb  32131  mettrifi  32150  heiborlem8  32214  heiborlem10  32216  heibor  32217  riscer  32291  igenval2  32363  lshpcmp  32625  eqlkr  32736  lkrlsp2  32740  lkrshp  32742  cvrnbtwn2  32912  cvlexch3  32969  cvlexch4N  32970  cvlatexchb1  32971  cvlsupr3  32981  exatleN  33040  cvratlem  33057  atcvrj2b  33068  cvrat3  33078  cvrat4  33079  athgt  33092  ps-1  33113  ps-2  33114  3atlem5  33123  3at  33126  llnneat  33150  llnmlplnN  33175  lplnneat  33181  lplnnelln  33182  islpln2a  33184  lplnriaN  33186  lplnribN  33187  lplnexllnN  33200  2llnjaN  33202  lvolnle3at  33218  lvolneatN  33224  lvolnelln  33225  lvolnelpln  33226  islvol2aN  33228  dalem62  33370  pmapglb2N  33407  pmapglb2xN  33408  lncmp  33419  paddasslem14  33469  paddasslem15  33470  pmod2iN  33485  hlmod1i  33492  pclfinclN  33586  osumcllem8N  33599  pexmidlem4N  33609  pl42lem1N  33615  pl42lem4N  33618  lhpexle1  33644  lhpexle2lem  33645  lhpmcvr5N  33663  lhpmcvr6N  33664  ltrneq  33785  trlnidatb  33814  cdleme0ex2N  33861  cdleme27a  34005  cdleme17d3  34134  cdlemeg46gfre  34170  cdleme48gfv1  34174  cdlemeg49lebilem  34177  cdlemf2  34200  cdlemf  34201  cdlemfnid  34202  trlord  34207  cdlemg31c  34337  cdlemg35  34351  trlcone  34366  tendoeq2  34412  cdlemj3  34461  cdlemk26b-3  34543  cdlemk33N  34547  cdleml3N  34616  cdlemn  34851  dih1dimb2  34880  dihord5apre  34901  dihmeetlem1N  34929  dihglblem5apreN  34930  dihglblem2N  34933  dihglblem3N  34934  dihmeetlem13N  34958  dihmeetlem15N  34960  dihatexv  34977  hdmap14lem12  35521  oddcomabszz  35863  jm2.19lem4  35918  fiuneneq  36142  idomsubgmo  36143  pwinfi3  36238  binomcxplemnn0  36768  addrcom  36898  int3  37059  suctrALT  37285  suctrALTcf  37382  suctrALT3  37384  chordthmALT  37393  iunconlem2  37395  stoweidlem26  37998  stoweidlem34  38007  upgredg2vtx  39392  usgredg2vtxeuALT  39463  sizusglecusg  39689  nnsgrp  40325  ply1mulgsumlem1  40686
  Copyright terms: Public domain W3C validator