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

Theorem 3expia 1143
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expia ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1142 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32expr 446 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  ad5ant125  1473  mp3an3  1567  3gencl  3431  moi  3587  disji  4829  disjord  4833  3optocl  5399  sossfld  5791  f1oresrab  6617  soisores  6801  isomin  6811  isofrlem  6814  ovmpt2s  7014  ov2gf  7015  ndmovord  7054  nnsuc  7312  poxp  7523  brtpos  7596  dfsmo2  7680  smoiun  7694  smoord  7698  smogt  7700  omeulem1  7899  omeu  7902  oewordi  7908  uniinqs  8062  mapvalg  8102  pmvalg  8103  elmapg  8105  xpdom3  8297  mapdom3  8371  php3  8385  unxpdomlem3  8405  isinf  8412  findcard2  8439  isfinite2  8457  ordiso  8660  cnfcom3clem  8849  r111  8885  tskwe  9059  pr2ne  9111  infxpenlem  9119  dfac8alem  9135  infdif  9316  infdif2  9317  cff1  9365  coflim  9368  cfslbn  9374  cfslb2n  9375  cofsmo  9376  cfsmolem  9377  cfcoflem  9379  fin23lem27  9435  isf32lem9  9468  isf34lem6  9487  axcc2lem  9543  domtriomlem  9549  axdc4lem  9562  zorn2lem2  9604  axdclem2  9627  konigthlem  9675  gchen1  9732  gchen2  9733  gchpwdom  9777  gchaleph  9778  winainflem  9800  tskcard  9888  gruiun  9906  gruen  9919  intgru  9921  grudomon  9924  grur1a  9926  grutsk1  9928  nqereu  10036  nqereq  10042  ltsonq  10076  prlem934  10140  reclem3pr  10156  1re  10325  axsup  10398  addid2  10504  recex  10944  lemul1a  11162  lt2msq  11193  fimaxre2  11254  zdiv  11713  zextlt  11717  prime  11724  uzind2  11736  fzind  11741  lbzbi  11995  qbtwnxr  12249  qextltlem  12251  xralrple  12254  xltneg  12266  xlt2add  12308  supxrgtmnf  12377  ixxub  12414  ixxlb  12415  ioo0  12418  ico0  12439  ioc0  12440  icc0  12441  iocssre  12471  icossre  12472  iccssre  12473  fzen  12581  expclzlem  13107  expaddz  13127  expmulz  13129  hashgadd  13384  elovmpt2wrd  13559  ccatopth2  13695  cshf1  13780  shftuz  14032  cau3lem  14317  caubnd  14321  climuni  14506  lo1resb  14518  o1resb  14520  o1of2  14566  o1add  14567  o1mul  14568  o1sub  14569  ntrivcvgmul  14855  eflt  15067  moddvds  15214  dvdscmulr  15233  dvdsmulcr  15234  dvdsle  15255  divalglem8  15343  divalgb  15347  ndvdssub  15352  bitsfzo  15376  gcdcllem1  15440  gcdcllem3  15442  dvdsgcd  15480  lcmgcdlem  15538  lcmfeq0b  15562  qredeu  15590  isprm3  15614  prmdvdsexpr  15646  prmexpb  15647  eulerthlem2  15704  fermltl  15706  coprimeprodsq  15730  pythagtrip  15756  pcprendvds  15762  pcpremul  15765  pcdvdsb  15790  pc2dvds  15800  4sqlem12  15877  4sqlem18  15883  vdwlem10  15911  cshwshashlem3  16016  xpslem  16438  ismred  16467  mrieqv2d  16504  iscatd  16538  isfuncd  16729  fthestrcsetc  16995  fthsetcestrc  17010  poslubd  17353  dirtr  17441  mulgaddcom  17768  ghmrn  17875  pmtrprfv3  18075  mndodcongi  18163  oddvdsnn0  18164  oddvds  18167  odcl2  18183  odhash3  18192  gexdvds  18200  pgpfi  18221  lsmss1b  18281  lsmss2b  18283  efgsrel  18348  efgred  18362  cntzcmn  18446  cyggenod  18487  lt6abl  18497  gsumcom2  18575  pgpfac1lem2  18676  pgpfac1lem3  18678  dvdsunit  18865  unitmulclb  18867  irredrmul  18909  isabvd  19024  lmodvsdi  19090  lss0cl  19151  islbs3  19364  lbsextlem2  19368  mvrf1  19634  coe1fzgsumd  19880  gsummoncoe1  19882  evl1gsumd  19929  xrsdsreclblem  20000  scmataddcl  20533  scmatsubcl  20534  mdetunilem9  20637  mdetuni0  20638  mdetmul  20640  m2cpmrngiso  20776  pm2mpf1  20817  opnnei  21138  neindisj2  21141  cncls2  21291  cncls  21292  cnntr  21293  cnpresti  21306  cnprest  21307  lmcnp  21322  isreg2  21395  ordthauslem  21401  unconn  21446  2ndc1stc  21468  kgen2ss  21572  ptclsg  21632  cnmptcom  21695  kqfvima  21747  hmeof1o  21781  fbncp  21856  fbfinnfr  21858  trfbas2  21860  isufil2  21925  ufprim  21926  trufil  21927  filufint  21937  hausflim  21998  flimrest  22000  flimcls  22002  cnpfcf  22058  alexsubALT  22068  tmdgsum  22112  opnsubg  22124  cldsubg  22127  qustgpopn  22136  tsmsxp  22171  blpnf  22415  blssps  22442  blss  22443  blssec  22453  neibl  22519  prdsxmslem2  22547  xrsmopn  22828  metnrm  22878  climcncf  22916  iccpnfhmeo  22957  xrhmeo  22958  bndth  22970  cphsqrtcl3  23199  iscau2  23287  iscmet3lem2  23302  bcthlem5  23337  bcth3  23340  ishl2  23378  ivthlem1  23432  cmmbl  23515  iundisj2  23530  voliunlem2  23532  mbfaddlem  23641  itg2itg1  23717  itg2seq  23723  itg2mulclem  23727  cnplimc  23865  dvres2  23890  deg1nn0clb  24064  deg1lt0  24065  deg1ge  24072  plypf1  24182  plyadd  24187  plymul  24188  coeeu  24195  dgrub2  24205  coeidlem  24207  coeid3  24210  coemullem  24220  coe11  24223  coemulhi  24224  coemulc  24225  dgreq0  24235  dgrlt  24236  dgradd2  24238  vieta1lem2  24280  tanord1  24498  tanord  24499  logccne0  24539  cxpeq0  24638  cxpmul2z  24651  cxpcn3lem  24702  relogbzcl  24726  angpieqvd  24772  o1cxp  24915  scvxcvx  24926  chtublem  25150  bposlem3  25225  lgsqr  25290  dchrisumlema  25391  dchrisumlem2  25393  ostth2lem3  25538  iscgrglt  25623  tghilberti2  25747  inagswap  25944  f1otrg  25965  brbtwn2  25999  axpasch  26035  axcontlem4  26061  axcontlem5  26062  upgredg2vtx  26251  usgredg2vtxeuALT  26329  sizusglecusg  26587  upgredginwlk  26760  frgrwopreg1  27493  frgrwopreg2  27494  frgrregorufrg  27501  lpni  27663  ipasslem5  28018  htthlem  28102  omlsii  28590  spansni  28744  spansneleq  28757  elspansn4  28760  sumspansn  28836  homco1  28988  homulass  28989  mdsl0  29497  ssdmd1  29500  ssdmd2  29501  cvdmd  29524  chirredlem2  29578  atdmd  29585  atmd2  29587  disjif  29716  iundisj2f  29728  isoun  29806  padct  29824  iocinioc2  29868  iundisj2fi  29883  archiabllem1a  30070  archiabllem2a  30073  slmdvsdi  30093  ordtconnlem1  30295  indpi1  30407  measinblem  30608  measres  30610  measdivcstOLD  30612  mbfmco2  30652  orvclteinc  30862  sgn3da  30928  sgnnbi  30932  sgnpbi  30933  bnj605  31300  bnj607  31309  bnj964  31336  bnj1033  31360  bnj1128  31381  bnj1137  31386  bnj1136  31388  bnj1413  31426  bnj60  31453  cvmlift2lem10  31617  msubvrs  31780  wsuclem  32091  nosepon  32139  noextenddif  32142  nolesgn2o  32145  nosepne  32152  nodense  32163  dfrdg4  32379  brcolinear2  32486  brsegle2  32537  nn0prpw  32639  ntruni  32643  clsint2  32645  fnessref  32673  fnemeet2  32683  fnejoin2  32685  limsucncmpi  32761  ee7.2aOLD  32777  dissneqlem  33504  isbasisrelowllem1  33519  isbasisrelowllem2  33520  icoreclin  33521  poimirlem9  33731  poimirlem30  33752  poimirlem32  33754  areacirc  33817  filbcmb  33847  mettrifi  33864  heiborlem8  33928  heiborlem10  33930  heibor  33931  riscer  34098  igenval2  34176  lshpcmp  34768  eqlkr  34879  lkrlsp2  34883  lkrshp  34885  cvrnbtwn2  35055  cvlexch3  35112  cvlexch4N  35113  cvlatexchb1  35114  cvlsupr3  35124  exatleN  35184  cvratlem  35201  atcvrj2b  35212  cvrat3  35222  cvrat4  35223  athgt  35236  ps-1  35257  ps-2  35258  3atlem5  35267  3at  35270  llnneat  35294  llnmlplnN  35319  lplnneat  35325  lplnnelln  35326  islpln2a  35328  lplnriaN  35330  lplnribN  35331  lplnexllnN  35344  2llnjaN  35346  lvolnle3at  35362  lvolneatN  35368  lvolnelln  35369  lvolnelpln  35370  islvol2aN  35372  dalem62  35514  pmapglb2N  35551  pmapglb2xN  35552  lncmp  35563  paddasslem14  35613  paddasslem15  35614  pmod2iN  35629  hlmod1i  35636  pclfinclN  35730  osumcllem8N  35743  pexmidlem4N  35753  pl42lem1N  35759  pl42lem4N  35762  lhpexle1  35788  lhpexle2lem  35789  lhpmcvr5N  35807  lhpmcvr6N  35808  ltrneq  35929  trlnidatb  35958  cdleme0ex2N  36005  cdleme27a  36148  cdleme17d3  36277  cdlemeg46gfre  36313  cdleme48gfv1  36317  cdlemeg49lebilem  36320  cdlemf2  36343  cdlemf  36344  cdlemfnid  36345  trlord  36350  cdlemg31c  36480  cdlemg35  36494  trlcone  36509  tendoeq2  36555  cdlemj3  36604  cdlemk26b-3  36686  cdlemk33N  36690  cdleml3N  36759  cdlemn  36993  dih1dimb2  37022  dihord5apre  37043  dihmeetlem1N  37071  dihglblem5apreN  37072  dihglblem2N  37075  dihglblem3N  37076  dihmeetlem13N  37100  dihmeetlem15N  37102  dihatexv  37119  hdmap14lem12  37660  oddcomabszz  38010  jm2.19lem4  38060  fiuneneq  38276  idomsubgmo  38277  pwinfi3  38368  gneispa  38928  binomcxplemnn0  39048  addrcom  39177  int3  39335  suctrALT  39555  suctrALTcf  39652  suctrALT3  39654  chordthmALT  39663  iunconnlem2  39665  stoweidlem26  40722  stoweidlem34  40730  issald  41030  goldbachth  42034  nnsgrp  42385  ply1mulgsumlem1  42742
  Copyright terms: Public domain W3C validator