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

Theorem 3expia 1258
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expia ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 443 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  mp3an3  1404  3gencl  3209  moi  3355  disji  4564  3optocl  5109  sossfld  5484  f1oresrab  6286  soisores  6454  isomin  6464  isofrlem  6467  ovmpt2s  6659  ov2gf  6660  ndmovord  6699  nnsuc  6951  poxp  7153  brtpos  7225  dfsmo2  7308  smoiun  7322  smoord  7326  smogt  7328  omeulem1  7526  omeu  7529  oewordi  7535  uniinqs  7691  mapvalg  7731  pmvalg  7732  elmapg  7734  xpdom3  7920  mapdom3  7994  php3  8008  unxpdomlem3  8028  isinf  8035  findcard2  8062  isfinite2  8080  ordiso  8281  cnfcom3clem  8462  r111  8498  tskwe  8636  pr2ne  8688  infxpenlem  8696  dfac8alem  8712  infdif  8891  infdif2  8892  cff1  8940  coflim  8943  cfslbn  8949  cfslb2n  8950  cofsmo  8951  cfsmolem  8952  cfcoflem  8954  fin23lem27  9010  isf32lem9  9043  isf34lem6  9062  axcc2lem  9118  domtriomlem  9124  axdc4lem  9137  zorn2lem2  9179  axdclem2  9202  konigthlem  9246  gchen1  9303  gchen2  9304  gchpwdom  9348  gchaleph  9349  winainflem  9371  tskcard  9459  gruiun  9477  gruen  9490  intgru  9492  grudomon  9495  grur1a  9497  grutsk1  9499  nqereu  9607  nqereq  9613  ltsonq  9647  prlem934  9711  reclem3pr  9727  1re  9895  axsup  9964  addid2  10070  recex  10510  lemul1a  10728  lt2msq  10759  fimaxre2  10820  zdiv  11281  zextlt  11285  prime  11292  uzind2  11304  fzind  11309  lbzbi  11610  qbtwnxr  11866  qextltlem  11868  xralrple  11871  xltneg  11883  xlt2add  11921  supxrgtmnf  11989  ixxub  12025  ixxlb  12026  ioo0  12029  ico0  12050  ioc0  12051  icc0  12052  iocssre  12082  icossre  12083  iccssre  12084  fzen  12186  expclzlem  12703  expaddz  12723  expmulz  12725  hashgadd  12981  elovmpt2wrd  13150  ccatopth2  13271  cshf1  13355  shftuz  13605  cau3lem  13890  caubnd  13894  climuni  14079  lo1resb  14091  o1resb  14093  o1of2  14139  o1add  14140  o1mul  14141  o1sub  14142  ntrivcvgmul  14421  eflt  14634  moddvds  14777  dvdscmulr  14796  dvdsmulcr  14797  dvdsle  14818  divalglem8  14909  divalgb  14913  ndvdssub  14919  bitsfzo  14943  gcdcllem1  15007  gcdcllem3  15009  dvdsgcd  15047  lcmgcdlem  15105  lcmfeq0b  15129  qredeu  15158  isprm3  15182  prmdvdsexpr  15215  prmexpb  15216  eulerthlem2  15273  fermltl  15275  coprimeprodsq  15299  pythagtrip  15325  pcprendvds  15331  pcpremul  15334  pcdvdsb  15359  pc2dvds  15369  4sqlem12  15446  4sqlem18  15452  vdwlem10  15480  cshwshashlem3  15590  xpslem  16004  ismred  16033  mrieqv2d  16070  iscatd  16105  isfuncd  16296  fthestrcsetc  16561  fthsetcestrc  16576  poslubd  16919  dirtr  17007  mulgaddcom  17335  ghmrn  17444  pmtrprfv3  17645  mndodcongi  17733  oddvdsnn0  17734  oddvds  17737  odcl2  17753  odhash3  17762  gexdvds  17770  pgpfi  17791  lsmss1b  17851  lsmss2b  17853  efgsrel  17918  efgred  17932  cntzcmn  18016  cyggenod  18057  lt6abl  18067  gsumcom2  18145  pgpfac1lem2  18245  pgpfac1lem3  18247  dvdsunit  18434  unitmulclb  18436  irredrmul  18478  isabvd  18591  lmodvsdi  18657  lss0cl  18716  islbs3  18924  lbsextlem2  18928  mvrf1  19194  coe1fzgsumd  19441  gsummoncoe1  19443  evl1gsumd  19490  xrsdsreclblem  19559  scmataddcl  20088  scmatsubcl  20089  mdetunilem9  20192  mdetuni0  20193  mdetmul  20195  m2cpmrngiso  20329  pm2mpf1  20370  opnnei  20681  neindisj2  20684  cncls2  20834  cncls  20835  cnntr  20836  cnpresti  20849  cnprest  20850  lmcnp  20865  isreg2  20938  ordthauslem  20944  uncon  20989  2ndc1stc  21011  kgen2ss  21115  ptclsg  21175  cnmptcom  21238  kqfvima  21290  hmeof1o  21324  fbncp  21400  fbfinnfr  21402  trfbas2  21404  isufil2  21469  ufprim  21470  trufil  21471  filufint  21481  hausflim  21542  flimrest  21544  flimcls  21546  cnpfcf  21602  alexsubALT  21612  tmdgsum  21656  opnsubg  21668  cldsubg  21671  qustgpopn  21680  tsmsxp  21715  blpnf  21959  blssps  21986  blss  21987  blssec  21997  neibl  22063  prdsxmslem2  22091  xrsmopn  22370  metnrm  22420  climcncf  22458  iccpnfhmeo  22499  xrhmeo  22500  bndth  22512  cphsqrtcl3  22739  iscau2  22827  iscmet3lem2  22842  bcthlem5  22877  bcth3  22880  ishl2  22918  ivthlem1  22971  cmmbl  23053  iundisj2  23068  voliunlem2  23070  mbfaddlem  23177  itg2itg1  23253  itg2seq  23259  itg2mulclem  23263  cnplimc  23401  dvres2  23426  deg1nn0clb  23598  deg1lt0  23599  deg1ge  23606  plypf1  23716  plyadd  23721  plymul  23722  coeeu  23729  dgrub2  23739  coeidlem  23741  coeid3  23744  coemullem  23754  coe11  23757  coemulhi  23758  coemulc  23759  dgreq0  23769  dgrlt  23770  dgradd2  23772  vieta1lem2  23814  tanord1  24031  tanord  24032  logccne0  24073  cxpeq0  24168  cxpmul2z  24181  cxpcn3lem  24232  relogbzcl  24256  angpieqvd  24302  o1cxp  24445  scvxcvx  24456  chtublem  24680  bposlem3  24755  lgsqr  24820  dchrisumlema  24921  dchrisumlem2  24923  ostth2lem3  25068  iscgrglt  25154  tghilberti2  25278  inagswap  25475  f1otrg  25496  brbtwn2  25530  axpasch  25566  axcontlem4  25592  axcontlem5  25593  sizeusglecusg  25807  wwlkextproplem3  26064  lpni  26515  ipasslem5  26867  htthlem  26951  omlsii  27439  spansni  27593  spansneleq  27606  elspansn4  27609  sumspansn  27685  homco1  27837  homulass  27838  mdsl0  28346  ssdmd1  28349  ssdmd2  28350  cvdmd  28373  chirredlem2  28427  atdmd  28434  atmd2  28436  disjif  28566  iundisj2f  28578  isoun  28655  padct  28678  iocinioc2  28724  iundisj2fi  28736  archiabllem1a  28869  archiabllem2a  28872  slmdvsdi  28892  ordtconlem1  29091  indpi1  29204  measinblem  29403  measres  29405  measdivcstOLD  29407  mbfmco2  29447  orvclteinc  29657  sgn3da  29723  sgnnbi  29727  sgnpbi  29728  bnj605  30024  bnj607  30033  bnj964  30060  bnj1033  30084  bnj1128  30105  bnj1137  30110  bnj1136  30112  bnj1413  30150  bnj60  30177  cvmlift2lem10  30341  msubvrs  30504  wsuclem  30810  wsuclemOLD  30811  nosepon  30859  nodense  30881  dfrdg4  31021  brcolinear2  31128  brsegle2  31179  nn0prpw  31281  ntruni  31285  clsint2  31287  fnessref  31315  fnemeet2  31325  fnejoin2  31327  limsucncmpi  31407  ee7.2aOLD  31423  dissneqlem  32146  isbasisrelowllem1  32162  isbasisrelowllem2  32163  icoreclin  32164  poimirlem9  32371  poimirlem30  32392  poimirlem32  32394  areacirc  32458  filbcmb  32488  mettrifi  32506  heiborlem8  32570  heiborlem10  32572  heibor  32573  riscer  32740  igenval2  32818  lshpcmp  33076  eqlkr  33187  lkrlsp2  33191  lkrshp  33193  cvrnbtwn2  33363  cvlexch3  33420  cvlexch4N  33421  cvlatexchb1  33422  cvlsupr3  33432  exatleN  33491  cvratlem  33508  atcvrj2b  33519  cvrat3  33529  cvrat4  33530  athgt  33543  ps-1  33564  ps-2  33565  3atlem5  33574  3at  33577  llnneat  33601  llnmlplnN  33626  lplnneat  33632  lplnnelln  33633  islpln2a  33635  lplnriaN  33637  lplnribN  33638  lplnexllnN  33651  2llnjaN  33653  lvolnle3at  33669  lvolneatN  33675  lvolnelln  33676  lvolnelpln  33677  islvol2aN  33679  dalem62  33821  pmapglb2N  33858  pmapglb2xN  33859  lncmp  33870  paddasslem14  33920  paddasslem15  33921  pmod2iN  33936  hlmod1i  33943  pclfinclN  34037  osumcllem8N  34050  pexmidlem4N  34060  pl42lem1N  34066  pl42lem4N  34069  lhpexle1  34095  lhpexle2lem  34096  lhpmcvr5N  34114  lhpmcvr6N  34115  ltrneq  34236  trlnidatb  34265  cdleme0ex2N  34312  cdleme27a  34456  cdleme17d3  34585  cdlemeg46gfre  34621  cdleme48gfv1  34625  cdlemeg49lebilem  34628  cdlemf2  34651  cdlemf  34652  cdlemfnid  34653  trlord  34658  cdlemg31c  34788  cdlemg35  34802  trlcone  34817  tendoeq2  34863  cdlemj3  34912  cdlemk26b-3  34994  cdlemk33N  34998  cdleml3N  35067  cdlemn  35302  dih1dimb2  35331  dihord5apre  35352  dihmeetlem1N  35380  dihglblem5apreN  35381  dihglblem2N  35384  dihglblem3N  35385  dihmeetlem13N  35409  dihmeetlem15N  35411  dihatexv  35428  hdmap14lem12  35972  oddcomabszz  36310  jm2.19lem4  36360  fiuneneq  36577  idomsubgmo  36578  pwinfi3  36670  gneispa  37231  binomcxplemnn0  37353  addrcom  37483  int3  37641  suctrALT  37866  suctrALTcf  37963  suctrALT3  37965  chordthmALT  37974  iunconlem2  37976  stoweidlem26  38702  stoweidlem34  38710  goldbachth  39781  upgredg2vtx  40354  usgredg2vtxeuALT  40430  sizusglecusg  40660  nnsgrp  41588  ply1mulgsumlem1  41949
  Copyright terms: Public domain W3C validator