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

Theorem 3expib 1145
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 1141 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 398 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:  3anidm12  1535  mob  3597  eqbrrdva  5507  fco  6283  f1oiso2  6836  frxp  7531  onfununi  7684  smoel2  7706  smoiso2  7712  3ecoptocl  8084  dffi2  8578  elfiun  8585  dif1card  9126  infxpenlem  9129  cfeq0  9373  cfsuc  9374  cfflb  9376  cfslb2n  9385  cofsmo  9386  domtriomlem  9559  axdc3lem4  9570  axdc4lem  9572  ttukey2g  9633  tskxpss  9889  grudomon  9934  elnpi  10105  dedekind  10495  nn0n0n1ge2b  11645  fzind  11761  suprzcl2  12017  icoshft  12535  fzen  12601  hashbclem  13473  seqcoll  13485  relexpsucr  14012  relexpsucl  14016  relexpfld  14032  shftuz  14052  mulgcd  15504  algcvga  15531  lcmneg  15555  ressbas  16161  resslem  16164  ressress  16170  psss  17439  tsrlemax  17445  isnmgm  17471  gsummgmpropd  17500  iscmnd  18426  ring1ne0  18813  unitmulclb  18887  isdrngd  18996  issrngd  19085  rmodislmodlem  19154  rmodislmod  19155  abvn0b  19531  mpfaddcl  19762  mpfmulcl  19763  pf1addcl  19945  pf1mulcl  19946  isphld  20229  fitop  20939  hausnei2  21392  ordtt1  21418  locfincmp  21564  basqtop  21749  filfi  21897  fgcl  21916  neifil  21918  filuni  21923  cnextcn  22105  prdsmet  22409  blssps  22463  blss  22464  metcnp3  22579  hlhil  23449  volsup2  23609  sincosq1sgn  24488  sincosq2sgn  24489  sincosq3sgn  24490  sincosq4sgn  24491  sinq12ge0  24498  bcmono  25239  iswlkg  26760  umgrwwlks2on  27121  clwlkclwwlkfo  27175  3cyclfrgrrn1  27483  grpodivf  27744  ipf  27919  shintcli  28539  spanuni  28754  adjadj  29146  unopadj2  29148  hmopadj  29149  hmopbdoptHIL  29198  resvsca  30178  resvlem  30179  submateq  30223  esumcocn  30490  bnj1379  31246  bnj571  31321  bnj594  31327  bnj580  31328  bnj600  31334  bnj1189  31422  bnj1321  31440  bnj1384  31445  climuzcnv  31909  fness  32687  neificl  33879  metf1o  33881  isismty  33930  ismtybndlem  33935  ablo4pnp  34009  divrngcl  34086  keridl  34161  prnc  34196  lsmsatcv  34809  llncvrlpln2  35356  lplncvrlvol2  35414  linepsubN  35551  pmapsub  35567  dalawlem10  35679  dalawlem13  35682  dalawlem14  35683  dalaw  35685  diaf11N  36848  dibf11N  36960  ismrcd1  37781  ismrcd2  37782  mzpincl  37817  mzpadd  37821  mzpmul  37822  pellfundge  37966  imasgim  38189  stoweidlem2  40716  stoweidlem17  40731
  Copyright terms: Public domain W3C validator