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

Theorem 3expia 1113
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 1112 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32expr 457 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ad5ant125  1358  mp3an3  1441  3gencl  3534  moi  3706  disji  5040  disjord  5045  3optocl  5640  sossfld  6036  f1oresrab  6881  soisores  7069  isomin  7079  isofrlem  7082  ovmpos  7287  ov2gf  7288  ndmovord  7327  nnsuc  7586  poxp  7811  brtpos  7890  dfsmo2  7973  smoiun  7987  smoord  7991  smogt  7993  omeulem1  8197  omeu  8200  oewordi  8206  uniinqs  8366  mapvalg  8405  pmvalg  8406  elmapg  8408  xpdom3  8603  mapdom3  8677  php3  8691  unxpdomlem3  8712  isinf  8719  findcard2  8746  isfinite2  8764  ordiso  8968  cnfcom3clem  9156  r111  9192  tskwe  9367  pr2ne  9419  infxpenlem  9427  dfac8alem  9443  infdif  9619  infdif2  9620  cff1  9668  coflim  9671  cfslbn  9677  cfslb2n  9678  cofsmo  9679  cfsmolem  9680  cfcoflem  9682  fin23lem27  9738  isf32lem9  9771  isf34lem6  9790  axcc2lem  9846  domtriomlem  9852  axdc4lem  9865  zorn2lem2  9907  axdclem2  9930  konigthlem  9978  gchen1  10035  gchen2  10036  gchpwdom  10080  gchaleph  10081  winainflem  10103  tskcard  10191  gruiun  10209  gruen  10222  intgru  10224  grudomon  10227  grur1a  10229  grutsk1  10231  nqereu  10339  nqereq  10345  ltsonq  10379  prlem934  10443  reclem3pr  10459  1re  10629  axsup  10704  addid2  10811  recex  11260  lemul1a  11482  lt2msq  11513  fimaxre2  11574  zdiv  12040  zextlt  12044  prime  12051  uzind2  12063  fzind  12068  lbzbi  12324  qbtwnxr  12581  qextltlem  12583  xralrple  12586  xltneg  12598  xlt2add  12641  supxrgtmnf  12710  ixxub  12747  ixxlb  12748  ioo0  12751  ico0  12772  ioc0  12773  icc0  12774  iocssre  12804  icossre  12805  iccssre  12806  fzen  12912  expclzlem  13441  expaddz  13461  expmulz  13463  hashgadd  13726  hashunsngx  13742  hashgt23el  13773  elovmpowrd  13898  pfxnd0  14038  ccatopth2  14067  pfxccatin12  14083  cshf1  14160  shftuz  14416  cau3lem  14702  caubnd  14706  climuni  14897  lo1resb  14909  o1resb  14911  o1of2  14957  o1add  14958  o1mul  14959  o1sub  14960  ntrivcvgmul  15246  eflt  15458  moddvds  15606  dvdscmulr  15626  dvdsmulcr  15627  dvdsle  15648  divalglem8  15739  divalgb  15743  ndvdssub  15748  bitsfzo  15772  gcdcllem1  15836  gcdcllem3  15838  dvdsgcd  15880  lcmgcdlem  15938  lcmfeq0b  15962  qredeu  15990  isprm3  16015  prmdvdsexpr  16049  prmexpb  16050  eulerthlem2  16107  fermltl  16109  coprimeprodsq  16133  pythagtrip  16159  pcprendvds  16165  pcpremul  16168  pcdvdsb  16193  pc2dvds  16203  4sqlem12  16280  4sqlem18  16286  vdwlem10  16314  cshwshashlem3  16419  xpsrnbas  16832  ismred  16861  mrieqv2d  16898  iscatd  16932  isfuncd  17123  fthestrcsetc  17388  fthsetcestrc  17403  poslubd  17746  dirtr  17834  mulgaddcom  18189  ghmrn  18309  pmtrprfv3  18511  mndodcongi  18600  oddvdsnn0  18601  oddvds  18604  odcl2  18621  odhash3  18630  gexdvds  18638  pgpfi  18659  lsmss1b  18721  lsmss2b  18723  efgsrel  18789  efgred  18803  cntzcmn  18889  cyggenod  18932  lt6abl  18944  gsumcom2  19024  pgpfac1lem2  19126  pgpfac1lem3  19128  dvdsunit  19342  unitmulclb  19344  irredrmul  19386  isabvd  19520  lmodvsdi  19586  lss0cl  19647  islbs3  19856  lbsextlem2  19860  mvrf1  20133  coe1fzgsumd  20398  gsummoncoe1  20400  evl1gsumd  20448  xrsdsreclblem  20519  scmataddcl  21053  scmatsubcl  21054  mdetunilem9  21157  mdetuni0  21158  mdetmul  21160  m2cpmrngiso  21294  pm2mpf1  21335  opnnei  21656  neindisj2  21659  cncls2  21809  cncls  21810  cnntr  21811  cnpresti  21824  cnprest  21825  lmcnp  21840  isreg2  21913  ordthauslem  21919  unconn  21965  2ndc1stc  21987  kgen2ss  22091  ptclsg  22151  cnmptcom  22214  kqfvima  22266  hmeof1o  22300  fbncp  22375  fbfinnfr  22377  trfbas2  22379  isufil2  22444  ufprim  22445  trufil  22446  filufint  22456  hausflim  22517  flimrest  22519  flimcls  22521  cnpfcf  22577  alexsubALT  22587  tmdgsum  22631  opnsubg  22643  cldsubg  22646  qustgpopn  22655  tsmsxp  22690  blpnf  22934  blssps  22961  blss  22962  blssec  22972  neibl  23038  prdsxmslem2  23066  xrsmopn  23347  metnrm  23397  climcncf  23435  iccpnfhmeo  23476  xrhmeo  23477  bndth  23489  cphsqrtcl3  23718  iscau2  23807  iscmet3lem2  23822  bcthlem5  23858  bcth3  23861  ishl2  23900  ivthlem1  23979  cmmbl  24062  iundisj2  24077  voliunlem2  24079  mbfaddlem  24188  itg2itg1  24264  itg2seq  24270  itg2mulclem  24274  cnplimc  24412  dvres2  24437  deg1nn0clb  24611  deg1lt0  24612  deg1ge  24619  plypf1  24729  plyadd  24734  plymul  24735  coeeu  24742  dgrub2  24752  coeidlem  24754  coeid3  24757  coemullem  24767  coe11  24770  coemulhi  24771  coemulc  24772  dgreq0  24782  dgrlt  24783  dgradd2  24785  vieta1lem2  24827  tanord1  25048  tanord  25049  logccne0  25089  cxpeq0  25188  cxpmul2z  25201  cxpcn3lem  25255  relogbzcl  25279  angpieqvd  25336  o1cxp  25479  scvxcvx  25490  chtublem  25714  bposlem3  25789  lgsqr  25854  2sqnn  25942  dchrisumlema  25991  dchrisumlem2  25993  ostth2lem3  26138  tghilberti2  26351  inagswap  26554  f1otrg  26584  brbtwn2  26618  axpasch  26654  axcontlem4  26680  axcontlem5  26681  upgredg2vtx  26853  usgredg2vtxeuALT  26931  sizusglecusg  27172  upgredginwlk  27344  frgrwopreg1  28024  frgrwopreg2  28025  frgrregorufrg  28032  lpni  28184  ipasslem5  28539  htthlem  28621  omlsii  29107  spansni  29261  spansneleq  29274  elspansn4  29277  sumspansn  29353  homco1  29505  homulass  29506  mdsl0  30014  ssdmd1  30017  ssdmd2  30018  cvdmd  30041  chirredlem2  30095  atdmd  30102  atmd2  30104  disjif  30256  iundisj2f  30268  isoun  30363  padct  30381  iocinioc2  30428  iundisj2fi  30446  archiabllem1a  30747  archiabllem2a  30750  slmdvsdi  30770  ordtconnlem1  31066  indpi1  31178  measinblem  31378  measres  31380  measdivcstALTV  31383  mbfmco2  31422  orvclteinc  31632  sgn3da  31698  sgnnbi  31702  sgnpbi  31703  bnj605  32078  bnj607  32087  bnj964  32114  bnj1033  32138  bnj1128  32159  bnj1137  32164  bnj1136  32166  bnj1413  32204  bnj60  32231  cusgredgex  32265  subgrwlk  32276  acycgr1v  32293  cvmlift2lem10  32456  msubvrs  32704  wsuclem  33009  nosepon  33069  noextenddif  33072  nolesgn2o  33075  nosepne  33082  nodense  33093  dfrdg4  33309  brcolinear2  33416  brsegle2  33467  nn0prpw  33568  ntruni  33572  clsint2  33574  fnessref  33602  fnemeet2  33612  fnejoin2  33614  limsucncmpi  33690  ee7.2aOLD  33706  bj-idreseq  34346  dissneqlem  34503  isbasisrelowllem1  34518  isbasisrelowllem2  34519  icoreclin  34520  poimirlem9  34782  poimirlem30  34803  poimirlem32  34805  areacirc  34868  filbcmb  34896  mettrifi  34913  heiborlem8  34977  heiborlem10  34979  heibor  34980  riscer  35147  igenval2  35225  lshpcmp  36004  eqlkr  36115  lkrlsp2  36119  lkrshp  36121  cvrnbtwn2  36291  cvlexch3  36348  cvlexch4N  36349  cvlatexchb1  36350  cvlsupr3  36360  exatleN  36420  cvratlem  36437  atcvrj2b  36448  cvrat3  36458  cvrat4  36459  athgt  36472  ps-1  36493  ps-2  36494  3atlem5  36503  3at  36506  llnneat  36530  llnmlplnN  36555  lplnneat  36561  lplnnelln  36562  islpln2a  36564  lplnriaN  36566  lplnribN  36567  lplnexllnN  36580  2llnjaN  36582  lvolnle3at  36598  lvolneatN  36604  lvolnelln  36605  lvolnelpln  36606  islvol2aN  36608  dalem62  36750  pmapglb2N  36787  pmapglb2xN  36788  lncmp  36799  paddasslem14  36849  paddasslem15  36850  pmod2iN  36865  hlmod1i  36872  pclfinclN  36966  osumcllem8N  36979  pexmidlem4N  36989  pl42lem1N  36995  pl42lem4N  36998  lhpexle1  37024  lhpexle2lem  37025  lhpmcvr5N  37043  lhpmcvr6N  37044  ltrneq  37165  trlnidatb  37193  cdleme0ex2N  37240  cdleme27a  37383  cdleme17d3  37512  cdlemeg46gfre  37548  cdleme48gfv1  37552  cdlemeg49lebilem  37555  cdlemf2  37578  cdlemf  37579  cdlemfnid  37580  trlord  37585  cdlemg31c  37715  cdlemg35  37729  trlcone  37744  tendoeq2  37790  cdlemj3  37839  cdlemk26b-3  37921  cdlemk33N  37925  cdleml3N  37994  cdlemn  38228  dih1dimb2  38257  dihord5apre  38278  dihmeetlem1N  38306  dihglblem5apreN  38307  dihglblem2N  38310  dihglblem3N  38311  dihmeetlem13N  38335  dihmeetlem15N  38337  dihatexv  38354  hdmap14lem12  38895  frlmfzowrdb  39021  nn0rppwr  39060  nn0expgcd  39062  rtprmirr  39072  oddcomabszz  39419  jm2.19lem4  39467  fiuneneq  39675  idomsubgmo  39676  pwinfi3  39800  gneispa  40358  grumnudlem  40498  binomcxplemnn0  40558  addrcom  40684  int3  40823  suctrALT  41037  suctrALTcf  41133  suctrALT3  41135  chordthmALT  41144  iunconnlem2  41146  stoweidlem26  42188  stoweidlem34  42196  issald  42493  goldbachth  43586  nnsgrp  43961  ply1mulgsumlem1  44368
  Copyright terms: Public domain W3C validator