Theorem 3expib 1287

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1283	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 446	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

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:  3anidm12  1423  mob  3421  eqbrrdva  5324  fco  6096  f1oiso2  6642  frxp  7332  onfununi  7483  smoel2  7505  smoiso2  7511  3ecoptocl  7882  dffi2  8370  elfiun  8377  dif1card  8871  infxpenlem  8874  cfeq0  9116  cfsuc  9117  cfflb  9119  cfslb2n  9128  cofsmo  9129  domtriomlem  9302  axdc3lem4  9313  axdc4lem  9315  ttukey2g  9376  tskxpss  9632  grudomon  9677  elnpi  9848  dedekind  10238  nn0n0n1ge2b  11397  fzind  11513  suprzcl2  11816  icoshft  12332  fzen  12396  hashbclem  13274  seqcoll  13286  relexpsucr  13813  relexpsucl  13817  relexpfld  13833  shftuz  13853  mulgcd  15312  algcvga  15339  lcmneg  15363  ressbas  15977  resslem  15980  ressress  15985  psss  17261  tsrlemax  17267  isnmgm  17293  gsummgmpropd  17322  iscmnd  18251  ring1ne0  18637  unitmulclb  18711  isdrngd  18820  issrngd  18909  rmodislmodlem  18978  rmodislmod  18979  abvn0b  19350  mpfaddcl  19582  mpfmulcl  19583  pf1addcl  19765  pf1mulcl  19766  isphld  20047  fitop  20753  hausnei2  21205  ordtt1  21231  locfincmp  21377  basqtop  21562  filfi  21710  fgcl  21729  neifil  21731  filuni  21736  cnextcn  21918  prdsmet  22222  blssps  22276  blss  22277  metcnp3  22392  hlhil  23260  volsup2  23419  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  sinq12ge0  24305  bcmono  25047  iswlkg  26565  umgrwwlks2on  26923  3cyclfrgrrn1  27265  grpodivf  27520  ipf  27696  shintcli  28316  spanuni  28531  adjadj  28923  unopadj2  28925  hmopadj  28926  hmopbdoptHIL  28975  resvsca  29958  resvlem  29959  submateq  30003  esumcocn  30270  bnj1379  31027  bnj571  31102  bnj594  31108  bnj580  31109  bnj600  31115  bnj1189  31203  bnj1321  31221  bnj1384  31226  climuzcnv  31691  fness  32469  neificl  33679  metf1o  33681  isismty  33730  ismtybndlem  33735  ablo4pnp  33809  divrngcl  33886  keridl  33961  prnc  33996  lsmsatcv  34615  llncvrlpln2  35161  lplncvrlvol2  35219  linepsubN  35356  pmapsub  35372  dalawlem10  35484  dalawlem13  35487  dalawlem14  35488  dalaw  35490  diaf11N  36655  dibf11N  36767  ismrcd1  37578  ismrcd2  37579  mzpincl  37614  mzpadd  37618  mzpmul  37619  pellfundge  37763  imasgim  37987  stoweidlem2  40537  stoweidlem17  40552