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

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

Proof of Theorem 3expib
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1116 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 414 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3anidm12  1416  mob  3694  eqbrrdva  5727  fco  6521  f1oiso2  7098  frxp  7816  onfununi  7974  smoel2  7996  smoiso2  8002  3ecoptocl  8385  dffi2  8884  elfiun  8891  dif1card  9434  infxpenlem  9437  cfeq0  9676  cfsuc  9677  cfflb  9679  cfslb2n  9688  cofsmo  9689  domtriomlem  9862  axdc3lem4  9873  axdc4lem  9875  ttukey2g  9936  tskxpss  10192  grudomon  10237  elnpi  10408  dedekind  10801  nn0n0n1ge2b  11960  fzind  12077  suprzcl2  12335  icoshft  12860  fzen  12928  hashgt23el  13790  hashbclem  13815  seqcoll  13827  relexpsucr  14388  relexpsucl  14392  relexpfld  14408  shftuz  14428  mulgcd  15894  algcvga  15921  lcmneg  15945  ressbas  16554  resslem  16557  ressress  16562  psss  17824  tsrlemax  17830  isnmgm  17856  gsummgmpropd  17891  iscmnd  18919  ring1ne0  19344  unitmulclb  19418  isdrngd  19527  issrngd  19632  rmodislmodlem  19701  rmodislmod  19702  abvn0b  20075  mpfaddcl  20318  mpfmulcl  20319  pf1addcl  20516  pf1mulcl  20517  isphld  20798  fitop  21508  hausnei2  21961  ordtt1  21987  locfincmp  22134  basqtop  22319  filfi  22467  fgcl  22486  neifil  22488  filuni  22493  cnextcn  22675  prdsmet  22980  blssps  23034  blss  23035  metcnp3  23150  hlhil  24050  volsup2  24212  sincosq1sgn  25094  sincosq2sgn  25095  sincosq3sgn  25096  sincosq4sgn  25097  sinq12ge0  25104  bcmono  25864  iswlkg  27406  umgrwwlks2on  27746  clwlkclwwlkfo  27797  3cyclfrgrrn1  28073  grpodivf  28324  ipf  28499  shintcli  29115  spanuni  29330  adjadj  29722  unopadj2  29724  hmopadj  29725  hmopbdoptHIL  29774  resvsca  30936  resvlem  30937  submateq  31134  esumcocn  31396  bnj1379  32159  bnj571  32235  bnj594  32241  bnj580  32242  bnj600  32248  bnj1189  32338  bnj1321  32356  bnj1384  32361  hashfundm  32411  f1resrcmplf1dlem  32416  cplgredgex  32424  cusgr3cyclex  32440  loop1cycl  32441  umgr2cycllem  32444  umgr2cycl  32445  acycgr2v  32454  cusgracyclt3v  32460  climuzcnv  32971  fness  33754  bj-idreseq  34522  bj-imdiridlem  34545  neificl  35136  metf1o  35138  isismty  35184  ismtybndlem  35189  ablo4pnp  35263  divrngcl  35340  keridl  35415  prnc  35450  lsmsatcv  36251  llncvrlpln2  36798  lplncvrlvol2  36856  linepsubN  36993  pmapsub  37009  dalawlem10  37121  dalawlem13  37124  dalawlem14  37125  dalaw  37127  diaf11N  38290  dibf11N  38402  ismrcd1  39555  ismrcd2  39556  mzpincl  39591  mzpadd  39595  mzpmul  39596  pellfundge  39739  imasgim  39960  sqrtcval  40257  stoweidlem2  42570  stoweidlem17  42585  imaelsetpreimafv  43838
  Copyright terms: Public domain W3C validator