Theorem 3expib 1118

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anidm12  1415  mob  3710  eqbrrdva  5742  fco  6533  f1oiso2  7107  frxp  7822  onfununi  7980  smoel2  8002  smoiso2  8008  3ecoptocl  8391  dffi2  8889  elfiun  8896  dif1card  9438  infxpenlem  9441  cfeq0  9680  cfsuc  9681  cfflb  9683  cfslb2n  9692  cofsmo  9693  domtriomlem  9866  axdc3lem4  9877  axdc4lem  9879  ttukey2g  9940  tskxpss  10196  grudomon  10241  elnpi  10412  dedekind  10805  nn0n0n1ge2b  11966  fzind  12083  suprzcl2  12341  icoshft  12862  fzen  12927  hashgt23el  13788  hashbclem  13813  seqcoll  13825  relexpsucr  14390  relexpsucl  14394  relexpfld  14410  shftuz  14430  mulgcd  15898  algcvga  15925  lcmneg  15949  ressbas  16556  resslem  16559  ressress  16564  psss  17826  tsrlemax  17832  isnmgm  17858  gsummgmpropd  17893  iscmnd  18921  ring1ne0  19343  unitmulclb  19417  isdrngd  19529  issrngd  19634  rmodislmodlem  19703  rmodislmod  19704  abvn0b  20077  mpfaddcl  20320  mpfmulcl  20321  pf1addcl  20518  pf1mulcl  20519  isphld  20800  fitop  21510  hausnei2  21963  ordtt1  21989  locfincmp  22136  basqtop  22321  filfi  22469  fgcl  22488  neifil  22490  filuni  22495  cnextcn  22677  prdsmet  22982  blssps  23036  blss  23037  metcnp3  23152  hlhil  24048  volsup2  24208  sincosq1sgn  25086  sincosq2sgn  25087  sincosq3sgn  25088  sincosq4sgn  25089  sinq12ge0  25096  bcmono  25855  iswlkg  27397  umgrwwlks2on  27738  clwlkclwwlkfo  27789  3cyclfrgrrn1  28066  grpodivf  28317  ipf  28492  shintcli  29108  spanuni  29323  adjadj  29715  unopadj2  29717  hmopadj  29718  hmopbdoptHIL  29767  resvsca  30905  resvlem  30906  submateq  31076  esumcocn  31341  bnj1379  32104  bnj571  32180  bnj594  32186  bnj580  32187  bnj600  32193  bnj1189  32283  bnj1321  32301  bnj1384  32306  hashfundm  32356  f1resrcmplf1dlem  32361  cplgredgex  32369  cusgr3cyclex  32385  loop1cycl  32386  umgr2cycllem  32389  umgr2cycl  32390  acycgr2v  32399  cusgracyclt3v  32405  climuzcnv  32916  fness  33699  bj-idreseq  34456  neificl  35030  metf1o  35032  isismty  35081  ismtybndlem  35086  ablo4pnp  35160  divrngcl  35237  keridl  35312  prnc  35347  lsmsatcv  36148  llncvrlpln2  36695  lplncvrlvol2  36753  linepsubN  36890  pmapsub  36906  dalawlem10  37018  dalawlem13  37021  dalawlem14  37022  dalaw  37024  diaf11N  38187  dibf11N  38299  ismrcd1  39302  ismrcd2  39303  mzpincl  39338  mzpadd  39342  mzpmul  39343  pellfundge  39486  imasgim  39707  stoweidlem2  42294  stoweidlem17  42309  imaelsetpreimafv  43562