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

Theorem 3expia 1286
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 1283 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 444 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  mp3an3  1453  3gencl  3268  moi  3422  disji  4669  disjord  4673  3optocl  5231  sossfld  5615  f1oresrab  6435  soisores  6617  isomin  6627  isofrlem  6630  ovmpt2s  6826  ov2gf  6827  ndmovord  6866  nnsuc  7124  poxp  7334  brtpos  7406  dfsmo2  7489  smoiun  7503  smoord  7507  smogt  7509  omeulem1  7707  omeu  7710  oewordi  7716  uniinqs  7870  mapvalg  7909  pmvalg  7910  elmapg  7912  xpdom3  8099  mapdom3  8173  php3  8187  unxpdomlem3  8207  isinf  8214  findcard2  8241  isfinite2  8259  ordiso  8462  cnfcom3clem  8640  r111  8676  tskwe  8814  pr2ne  8866  infxpenlem  8874  dfac8alem  8890  infdif  9069  infdif2  9070  cff1  9118  coflim  9121  cfslbn  9127  cfslb2n  9128  cofsmo  9129  cfsmolem  9130  cfcoflem  9132  fin23lem27  9188  isf32lem9  9221  isf34lem6  9240  axcc2lem  9296  domtriomlem  9302  axdc4lem  9315  zorn2lem2  9357  axdclem2  9380  konigthlem  9428  gchen1  9485  gchen2  9486  gchpwdom  9530  gchaleph  9531  winainflem  9553  tskcard  9641  gruiun  9659  gruen  9672  intgru  9674  grudomon  9677  grur1a  9679  grutsk1  9681  nqereu  9789  nqereq  9795  ltsonq  9829  prlem934  9893  reclem3pr  9909  1re  10077  axsup  10151  addid2  10257  recex  10697  lemul1a  10915  lt2msq  10946  fimaxre2  11007  zdiv  11485  zextlt  11489  prime  11496  uzind2  11508  fzind  11513  lbzbi  11814  qbtwnxr  12069  qextltlem  12071  xralrple  12074  xltneg  12086  xlt2add  12128  supxrgtmnf  12197  ixxub  12234  ixxlb  12235  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  iocssre  12291  icossre  12292  iccssre  12293  fzen  12396  expclzlem  12924  expaddz  12944  expmulz  12946  hashgadd  13204  elovmpt2wrd  13380  ccatopth2  13517  cshf1  13602  shftuz  13853  cau3lem  14138  caubnd  14142  climuni  14327  lo1resb  14339  o1resb  14341  o1of2  14387  o1add  14388  o1mul  14389  o1sub  14390  ntrivcvgmul  14678  eflt  14891  moddvds  15038  dvdscmulr  15057  dvdsmulcr  15058  dvdsle  15079  divalglem8  15170  divalgb  15174  ndvdssub  15180  bitsfzo  15204  gcdcllem1  15268  gcdcllem3  15270  dvdsgcd  15308  lcmgcdlem  15366  lcmfeq0b  15390  qredeu  15419  isprm3  15443  prmdvdsexpr  15476  prmexpb  15477  eulerthlem2  15534  fermltl  15536  coprimeprodsq  15560  pythagtrip  15586  pcprendvds  15592  pcpremul  15595  pcdvdsb  15620  pc2dvds  15630  4sqlem12  15707  4sqlem18  15713  vdwlem10  15741  cshwshashlem3  15851  xpslem  16280  ismred  16309  mrieqv2d  16346  iscatd  16381  isfuncd  16572  fthestrcsetc  16837  fthsetcestrc  16852  poslubd  17195  dirtr  17283  mulgaddcom  17611  ghmrn  17720  pmtrprfv3  17920  mndodcongi  18008  oddvdsnn0  18009  oddvds  18012  odcl2  18028  odhash3  18037  gexdvds  18045  pgpfi  18066  lsmss1b  18126  lsmss2b  18128  efgsrel  18193  efgred  18207  cntzcmn  18291  cyggenod  18332  lt6abl  18342  gsumcom2  18420  pgpfac1lem2  18520  pgpfac1lem3  18522  dvdsunit  18709  unitmulclb  18711  irredrmul  18753  isabvd  18868  lmodvsdi  18934  lss0cl  18995  islbs3  19203  lbsextlem2  19207  mvrf1  19473  coe1fzgsumd  19720  gsummoncoe1  19722  evl1gsumd  19769  xrsdsreclblem  19840  scmataddcl  20370  scmatsubcl  20371  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  m2cpmrngiso  20611  pm2mpf1  20652  opnnei  20972  neindisj2  20975  cncls2  21125  cncls  21126  cnntr  21127  cnpresti  21140  cnprest  21141  lmcnp  21156  isreg2  21229  ordthauslem  21235  unconn  21280  2ndc1stc  21302  kgen2ss  21406  ptclsg  21466  cnmptcom  21529  kqfvima  21581  hmeof1o  21615  fbncp  21690  fbfinnfr  21692  trfbas2  21694  isufil2  21759  ufprim  21760  trufil  21761  filufint  21771  hausflim  21832  flimrest  21834  flimcls  21836  cnpfcf  21892  alexsubALT  21902  tmdgsum  21946  opnsubg  21958  cldsubg  21961  qustgpopn  21970  tsmsxp  22005  blpnf  22249  blssps  22276  blss  22277  blssec  22287  neibl  22353  prdsxmslem2  22381  xrsmopn  22662  metnrm  22712  climcncf  22750  iccpnfhmeo  22791  xrhmeo  22792  bndth  22804  cphsqrtcl3  23033  iscau2  23121  iscmet3lem2  23136  bcthlem5  23171  bcth3  23174  ishl2  23212  ivthlem1  23266  cmmbl  23348  iundisj2  23363  voliunlem2  23365  mbfaddlem  23472  itg2itg1  23548  itg2seq  23554  itg2mulclem  23558  cnplimc  23696  dvres2  23721  deg1nn0clb  23895  deg1lt0  23896  deg1ge  23903  plypf1  24013  plyadd  24018  plymul  24019  coeeu  24026  dgrub2  24036  coeidlem  24038  coeid3  24041  coemullem  24051  coe11  24054  coemulhi  24055  coemulc  24056  dgreq0  24066  dgrlt  24067  dgradd2  24069  vieta1lem2  24111  tanord1  24328  tanord  24329  logccne0  24370  cxpeq0  24469  cxpmul2z  24482  cxpcn3lem  24533  relogbzcl  24557  angpieqvd  24603  o1cxp  24746  scvxcvx  24757  chtublem  24981  bposlem3  25056  lgsqr  25121  dchrisumlema  25222  dchrisumlem2  25224  ostth2lem3  25369  iscgrglt  25454  tghilberti2  25578  inagswap  25775  f1otrg  25796  brbtwn2  25830  axpasch  25866  axcontlem4  25892  axcontlem5  25893  upgredg2vtx  26081  usgredg2vtxeuALT  26159  sizusglecusg  26415  upgredginwlk  26588  frgrwopreg1  27298  frgrwopreg2  27299  frgrregorufrg  27306  2clwwlk2clwwlklem2  27330  lpni  27462  ipasslem5  27818  htthlem  27902  omlsii  28390  spansni  28544  spansneleq  28557  elspansn4  28560  sumspansn  28636  homco1  28788  homulass  28789  mdsl0  29297  ssdmd1  29300  ssdmd2  29301  cvdmd  29324  chirredlem2  29378  atdmd  29385  atmd2  29387  disjif  29517  iundisj2f  29529  isoun  29607  padct  29625  iocinioc2  29669  iundisj2fi  29684  archiabllem1a  29873  archiabllem2a  29876  slmdvsdi  29896  ordtconnlem1  30098  indpi1  30210  measinblem  30411  measres  30413  measdivcstOLD  30415  mbfmco2  30455  orvclteinc  30665  sgn3da  30731  sgnnbi  30735  sgnpbi  30736  bnj605  31103  bnj607  31112  bnj964  31139  bnj1033  31163  bnj1128  31184  bnj1137  31189  bnj1136  31191  bnj1413  31229  bnj60  31256  cvmlift2lem10  31420  msubvrs  31583  wsuclem  31895  nosepon  31943  noextenddif  31946  nolesgn2o  31949  nosepne  31956  nodense  31967  dfrdg4  32183  brcolinear2  32290  brsegle2  32341  nn0prpw  32443  ntruni  32447  clsint2  32449  fnessref  32477  fnemeet2  32487  fnejoin2  32489  limsucncmpi  32569  ee7.2aOLD  32585  dissneqlem  33317  isbasisrelowllem1  33333  isbasisrelowllem2  33334  icoreclin  33335  poimirlem9  33548  poimirlem30  33569  poimirlem32  33571  areacirc  33635  filbcmb  33665  mettrifi  33683  heiborlem8  33747  heiborlem10  33749  heibor  33750  riscer  33917  igenval2  33995  lshpcmp  34593  eqlkr  34704  lkrlsp2  34708  lkrshp  34710  cvrnbtwn2  34880  cvlexch3  34937  cvlexch4N  34938  cvlatexchb1  34939  cvlsupr3  34949  exatleN  35008  cvratlem  35025  atcvrj2b  35036  cvrat3  35046  cvrat4  35047  athgt  35060  ps-1  35081  ps-2  35082  3atlem5  35091  3at  35094  llnneat  35118  llnmlplnN  35143  lplnneat  35149  lplnnelln  35150  islpln2a  35152  lplnriaN  35154  lplnribN  35155  lplnexllnN  35168  2llnjaN  35170  lvolnle3at  35186  lvolneatN  35192  lvolnelln  35193  lvolnelpln  35194  islvol2aN  35196  dalem62  35338  pmapglb2N  35375  pmapglb2xN  35376  lncmp  35387  paddasslem14  35437  paddasslem15  35438  pmod2iN  35453  hlmod1i  35460  pclfinclN  35554  osumcllem8N  35567  pexmidlem4N  35577  pl42lem1N  35583  pl42lem4N  35586  lhpexle1  35612  lhpexle2lem  35613  lhpmcvr5N  35631  lhpmcvr6N  35632  ltrneq  35753  trlnidatb  35782  cdleme0ex2N  35829  cdleme27a  35972  cdleme17d3  36101  cdlemeg46gfre  36137  cdleme48gfv1  36141  cdlemeg49lebilem  36144  cdlemf2  36167  cdlemf  36168  cdlemfnid  36169  trlord  36174  cdlemg31c  36304  cdlemg35  36318  trlcone  36333  tendoeq2  36379  cdlemj3  36428  cdlemk26b-3  36510  cdlemk33N  36514  cdleml3N  36583  cdlemn  36818  dih1dimb2  36847  dihord5apre  36868  dihmeetlem1N  36896  dihglblem5apreN  36897  dihglblem2N  36900  dihglblem3N  36901  dihmeetlem13N  36925  dihmeetlem15N  36927  dihatexv  36944  hdmap14lem12  37488  oddcomabszz  37826  jm2.19lem4  37876  fiuneneq  38092  idomsubgmo  38093  pwinfi3  38185  gneispa  38745  binomcxplemnn0  38865  addrcom  38996  int3  39154  suctrALT  39375  suctrALTcf  39472  suctrALT3  39474  chordthmALT  39483  iunconnlem2  39485  stoweidlem26  40561  stoweidlem34  40569  issald  40869  goldbachth  41784  nnsgrp  42142  ply1mulgsumlem1  42499
  Copyright terms: Public domain W3C validator