Theorem 3expib 1102

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 1099	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 402	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  3anidm12  1399  mob  3618  eqbrrdva  5583  fco  6355  f1oiso2  6922  frxp  7618  onfununi  7775  smoel2  7797  smoiso2  7803  3ecoptocl  8181  dffi2  8674  elfiun  8681  dif1card  9222  infxpenlem  9225  cfeq0  9468  cfsuc  9469  cfflb  9471  cfslb2n  9480  cofsmo  9481  domtriomlem  9654  axdc3lem4  9665  axdc4lem  9667  ttukey2g  9728  tskxpss  9984  grudomon  10029  elnpi  10200  dedekind  10595  nn0n0n1ge2b  11768  fzind  11886  suprzcl2  12145  icoshft  12668  fzen  12733  hashbclem  13613  seqcoll  13625  relexpsucr  14239  relexpsucl  14243  relexpfld  14259  shftuz  14279  mulgcd  15742  algcvga  15769  lcmneg  15793  ressbas  16400  resslem  16403  ressress  16408  psss  17672  tsrlemax  17678  isnmgm  17704  gsummgmpropd  17733  iscmnd  18668  ring1ne0  19054  unitmulclb  19128  isdrngd  19240  issrngd  19344  rmodislmodlem  19413  rmodislmod  19414  abvn0b  19786  mpfaddcl  20017  mpfmulcl  20018  pf1addcl  20208  pf1mulcl  20209  isphld  20490  fitop  21202  hausnei2  21655  ordtt1  21681  locfincmp  21828  basqtop  22013  filfi  22161  fgcl  22180  neifil  22182  filuni  22187  cnextcn  22369  prdsmet  22673  blssps  22727  blss  22728  metcnp3  22843  hlhil  23739  volsup2  23899  sincosq1sgn  24777  sincosq2sgn  24778  sincosq3sgn  24779  sincosq4sgn  24780  sinq12ge0  24787  bcmono  25545  iswlkg  27088  umgrwwlks2on  27453  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  3cyclfrgrrn1  27809  grpodivf  28082  ipf  28257  shintcli  28877  spanuni  29092  adjadj  29484  unopadj2  29486  hmopadj  29487  hmopbdoptHIL  29536  resvsca  30538  resvlem  30539  submateq  30673  esumcocn  30940  bnj1379  31711  bnj571  31786  bnj594  31792  bnj580  31793  bnj600  31799  bnj1189  31887  bnj1321  31905  bnj1384  31910  climuzcnv  32374  fness  33158  neificl  34418  metf1o  34420  isismty  34469  ismtybndlem  34474  ablo4pnp  34548  divrngcl  34625  keridl  34700  prnc  34735  lsmsatcv  35539  llncvrlpln2  36086  lplncvrlvol2  36144  linepsubN  36281  pmapsub  36297  dalawlem10  36409  dalawlem13  36412  dalawlem14  36413  dalaw  36415  diaf11N  37578  dibf11N  37690  ismrcd1  38635  ismrcd2  38636  mzpincl  38671  mzpadd  38675  mzpmul  38676  pellfundge  38820  imasgim  39041  stoweidlem2  41664  stoweidlem17  41679