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

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

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  3656  eqbrrdva  5704  fco  6505  f1oiso2  7084  frxp  7803  onfununi  7961  smoel2  7983  smoiso2  7989  3ecoptocl  8372  dffi2  8871  elfiun  8878  dif1card  9421  infxpenlem  9424  cfeq0  9667  cfsuc  9668  cfflb  9670  cfslb2n  9679  cofsmo  9680  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  ttukey2g  9927  tskxpss  10183  grudomon  10228  elnpi  10399  dedekind  10792  nn0n0n1ge2b  11951  fzind  12068  suprzcl2  12326  icoshft  12851  fzen  12919  hashgt23el  13781  hashbclem  13806  seqcoll  13818  relexpsucl  14382  relexpsucr  14383  relexpfld  14400  shftuz  14420  mulgcd  15886  algcvga  15913  lcmneg  15937  ressbas  16546  resslem  16549  ressress  16554  psss  17816  tsrlemax  17822  isnmgm  17848  gsummgmpropd  17883  iscmnd  18911  ring1ne0  19337  unitmulclb  19411  isdrngd  19520  issrngd  19625  rmodislmodlem  19694  rmodislmod  19695  abvn0b  20068  isphld  20343  mpfaddcl  20777  mpfmulcl  20778  pf1addcl  20977  pf1mulcl  20978  fitop  21505  hausnei2  21958  ordtt1  21984  locfincmp  22131  basqtop  22316  filfi  22464  fgcl  22483  neifil  22485  filuni  22490  cnextcn  22672  prdsmet  22977  blssps  23031  blss  23032  metcnp3  23147  hlhil  24047  volsup2  24209  sincosq1sgn  25091  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  sinq12ge0  25101  bcmono  25861  iswlkg  27403  umgrwwlks2on  27743  clwlkclwwlkfo  27794  3cyclfrgrrn1  28070  grpodivf  28321  ipf  28496  shintcli  29112  spanuni  29327  adjadj  29719  unopadj2  29721  hmopadj  29722  hmopbdoptHIL  29771  resvsca  30954  resvlem  30955  submateq  31162  esumcocn  31449  bnj1379  32212  bnj571  32288  bnj594  32294  bnj580  32295  bnj600  32301  bnj1189  32391  bnj1321  32409  bnj1384  32414  hashfundm  32464  f1resrcmplf1dlem  32469  cplgredgex  32480  cusgr3cyclex  32496  loop1cycl  32497  umgr2cycllem  32500  umgr2cycl  32501  acycgr2v  32510  cusgracyclt3v  32516  climuzcnv  33027  fness  33810  bj-idreseq  34577  bj-imdiridlem  34600  neificl  35191  metf1o  35193  isismty  35239  ismtybndlem  35244  ablo4pnp  35318  divrngcl  35395  keridl  35470  prnc  35505  lsmsatcv  36306  llncvrlpln2  36853  lplncvrlvol2  36911  linepsubN  37048  pmapsub  37064  dalawlem10  37176  dalawlem13  37179  dalawlem14  37180  dalaw  37182  diaf11N  38345  dibf11N  38457  ismrcd1  39639  ismrcd2  39640  mzpincl  39675  mzpadd  39679  mzpmul  39680  pellfundge  39823  imasgim  40044  sqrtcval  40341  stoweidlem2  42644  stoweidlem17  42659  imaelsetpreimafv  43912