Theorem 3expib 1259

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3anidm12  1374  mob  3354  eqbrrdva  5201  fco  5957  f1oiso2  6480  frxp  7152  onfununi  7303  smoel2  7325  smoiso2  7331  3ecoptocl  7704  dffi2  8190  elfiun  8197  dif1card  8694  infxpenlem  8697  cfeq0  8939  cfsuc  8940  cfflb  8942  cfslb2n  8951  cofsmo  8952  domtriomlem  9125  axdc3lem4  9136  axdc4lem  9138  ttukey2g  9199  tskxpss  9451  grudomon  9496  elnpi  9667  dedekind  10052  nn0n0n1ge2b  11209  fzind  11310  suprzcl2  11613  icoshft  12124  fzen  12187  hashbclem  13048  seqcoll  13060  relexpsucr  13566  relexpsucl  13570  relexpfld  13586  shftuz  13606  mulgcd  15052  algcvga  15079  lcmneg  15103  ressbas  15706  resslem  15709  ressress  15714  psss  16986  tsrlemax  16992  isnmgm  17018  gsummgmpropd  17047  iscmnd  17977  ring1ne0  18363  unitmulclb  18437  isdrngd  18544  issrngd  18633  abvn0b  19072  mpfaddcl  19304  mpfmulcl  19305  pf1addcl  19487  pf1mulcl  19488  isphld  19766  fitop  20478  hausnei2  20915  ordtt1  20941  locfincmp  21087  basqtop  21272  filfi  21421  fgcl  21440  neifil  21442  filuni  21447  cnextcn  21629  prdsmet  21933  blssps  21987  blss  21988  metcnp3  22103  hlhil  22967  volsup2  23124  sincosq1sgn  23999  sincosq2sgn  24000  sincosq3sgn  24001  sincosq4sgn  24002  sinq12ge0  24009  bcmono  24747  usg2wlkonot  26204  3cyclfrgrarn1  26333  grpodivf  26570  ipf  26784  sspival  26809  shintcli  27406  spanuni  27621  adjadj  28013  unopadj2  28015  hmopadj  28016  hmopbdoptHIL  28065  resvsca  28995  resvlem  28996  submateq  29037  esumcocn  29303  bnj1379  29989  bnj571  30064  bnj594  30070  bnj580  30071  bnj600  30077  bnj1189  30165  bnj1321  30183  bnj1384  30188  climuzcnv  30653  fness  31348  neificl  32543  metf1o  32545  isismty  32594  ismtybndlem  32599  ablo4pnp  32673  divrngcl  32750  keridl  32825  prnc  32860  lsmsatcv  33139  llncvrlpln2  33685  lplncvrlvol2  33743  linepsubN  33880  pmapsub  33896  dalawlem10  34008  dalawlem13  34011  dalawlem14  34012  dalaw  34014  diaf11N  35180  dibf11N  35292  ismrcd1  36103  ismrcd2  36104  mzpincl  36139  mzpadd  36143  mzpmul  36144  pellfundge  36288  imasgim  36512  stoweidlem2  38719  stoweidlem17  38734  uhgrauhgrbi  40316  is1wlkg  40838  uspgrn2crct  41033  umgrwwlks2on  41183  3cyclfrgrrn1  41477