Theorem 3expib 1122

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anidm12  1421  mob  3700  dfss2  3944  eqbrrdva  5849  f1oiso2  7344  frxp  8123  onfununi  8353  smoel2  8375  smoiso2  8381  3ecoptocl  8821  ssfi  9185  f1domfi  9193  rex2dom  9252  fodomfib  9339  dffi2  9433  elfiun  9440  dif1card  10022  infxpenlem  10025  cfeq0  10268  cfsuc  10269  cfflb  10271  cfslb2n  10280  cofsmo  10281  domtriomlem  10454  axdc3lem4  10465  axdc4lem  10467  ttukey2g  10528  tskxpss  10784  grudomon  10829  elnpi  11000  dedekind  11396  nn0n0n1ge2b  12568  fzind  12689  suprzcl2  12952  icoshft  13488  fzen  13556  hashgt23el  14440  hashfundm  14458  hashbclem  14468  seqcoll  14480  relexpsucl  15048  relexpsucr  15049  relexpfld  15066  shftuz  15086  mulgcd  16565  algcvga  16596  lcmneg  16620  ressbas  17255  resseqnbas  17261  ressress  17266  psss  18588  tsrlemax  18594  isnmgm  18620  gsummgmpropd  18657  issgrpd  18706  iscmnd  19773  ring1ne0  20257  unitmulclb  20339  isdrngd  20723  isdrngdOLD  20725  abvn0b  20794  issrngd  20813  rmodislmodlem  20884  rmodislmod  20885  isphld  21612  mpfaddcl  22061  mpfmulcl  22062  pf1addcl  22289  pf1mulcl  22290  fitop  22836  hausnei2  23289  ordtt1  23315  locfincmp  23462  basqtop  23647  filfi  23795  fgcl  23814  neifil  23816  filuni  23821  cnextcn  24003  prdsmet  24307  blssps  24361  blss  24362  metcnp3  24477  hlhil  25393  volsup2  25556  sincosq1sgn  26457  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  sinq12ge0  26467  bcmono  27238  iswlkg  29539  umgrwwlks2on  29885  clwlkclwwlkfo  29936  3cyclfrgrrn1  30212  grpodivf  30465  ipf  30640  shintcli  31256  spanuni  31471  adjadj  31863  unopadj2  31865  hmopadj  31866  hmopbdoptHIL  31915  resvsca  33294  resvlem  33295  submateq  33786  esumcocn  34057  bnj1379  34807  bnj571  34883  bnj594  34889  bnj580  34890  bnj600  34896  bnj1189  34986  bnj1321  35004  bnj1384  35009  f1resrcmplf1dlem  35063  cplgredgex  35089  cusgr3cyclex  35104  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  acycgr2v  35118  cusgracyclt3v  35124  climuzcnv  35639  fness  36313  bj-idreseq  37126  bj-imdiridlem  37149  neificl  37723  metf1o  37725  isismty  37771  ismtybndlem  37776  ablo4pnp  37850  divrngcl  37927  keridl  38002  prnc  38037  lsmsatcv  38974  llncvrlpln2  39522  lplncvrlvol2  39580  linepsubN  39717  pmapsub  39733  dalawlem10  39845  dalawlem13  39848  dalawlem14  39849  dalaw  39851  diaf11N  41014  dibf11N  41126  ismrcd1  42668  ismrcd2  42669  mzpincl  42704  mzpadd  42708  mzpmul  42709  pellfundge  42852  imasgim  43071  sqrtcval  43612  stoweidlem2  45979  stoweidlem17  45994  imaelsetpreimafv  47357  opnneir  48829  i0oii  48842  io1ii  48843