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  3672  dfss2  3916  eqbrrdva  5813  f1oiso2  7292  frxp  8062  onfununi  8267  smoel2  8289  smoiso2  8295  3ecoptocl  8739  ssfi  9089  f1domfi  9097  rex2dom  9144  fodomfib  9220  dffi2  9314  elfiun  9321  dif1card  9908  infxpenlem  9911  cfeq0  10154  cfsuc  10155  cfflb  10157  cfslb2n  10166  cofsmo  10167  domtriomlem  10340  axdc3lem4  10351  axdc4lem  10353  ttukey2g  10414  tskxpss  10670  grudomon  10715  elnpi  10886  dedekind  11283  nn0n0n1ge2b  12457  fzind  12577  suprzcl2  12838  icoshft  13375  fzen  13443  hashgt23el  14333  hashfundm  14351  hashbclem  14361  seqcoll  14373  relexpsucl  14940  relexpsucr  14941  relexpfld  14958  shftuz  14978  mulgcd  16461  algcvga  16492  lcmneg  16516  ressbas  17149  resseqnbas  17155  ressress  17160  psss  18488  tsrlemax  18494  isnmgm  18554  gsummgmpropd  18591  issgrpd  18640  iscmnd  19708  ring1ne0  20219  unitmulclb  20301  isdrngd  20682  isdrngdOLD  20684  abvn0b  20753  issrngd  20772  rmodislmodlem  20864  rmodislmod  20865  isphld  21593  mpfaddcl  22041  mpfmulcl  22042  pf1addcl  22269  pf1mulcl  22270  fitop  22816  hausnei2  23269  ordtt1  23295  locfincmp  23442  basqtop  23627  filfi  23775  fgcl  23794  neifil  23796  filuni  23801  cnextcn  23983  prdsmet  24286  blssps  24340  blss  24341  metcnp3  24456  hlhil  25371  volsup2  25534  sincosq1sgn  26435  sincosq2sgn  26436  sincosq3sgn  26437  sincosq4sgn  26438  sinq12ge0  26445  bcmono  27216  n0cutlt  28286  iswlkg  29594  usgrwwlks2on  29938  umgrwwlks2on  29939  clwlkclwwlkfo  29991  3cyclfrgrrn1  30267  grpodivf  30520  ipf  30695  shintcli  31311  spanuni  31526  adjadj  31918  unopadj2  31920  hmopadj  31921  hmopbdoptHIL  31970  resvsca  33304  resvlem  33305  submateq  33843  esumcocn  34114  bnj1379  34863  bnj571  34939  bnj594  34945  bnj580  34946  bnj600  34952  bnj1189  35042  bnj1321  35060  bnj1384  35065  f1resrcmplf1dlem  35119  trssfir1om  35143  trssfir1omregs  35153  cplgredgex  35186  cusgr3cyclex  35201  loop1cycl  35202  umgr2cycllem  35205  umgr2cycl  35206  acycgr2v  35215  cusgracyclt3v  35221  climuzcnv  35736  fness  36414  bj-idreseq  37227  bj-imdiridlem  37250  neificl  37813  metf1o  37815  isismty  37861  ismtybndlem  37866  ablo4pnp  37940  divrngcl  38017  keridl  38092  prnc  38127  lsmsatcv  39129  llncvrlpln2  39676  lplncvrlvol2  39734  linepsubN  39871  pmapsub  39887  dalawlem10  39999  dalawlem13  40002  dalawlem14  40003  dalaw  40005  diaf11N  41168  dibf11N  41280  ismrcd1  42815  ismrcd2  42816  mzpincl  42851  mzpadd  42855  mzpmul  42856  pellfundge  42999  imasgim  43217  sqrtcval  43758  stoweidlem2  46124  stoweidlem17  46139  imaelsetpreimafv  47519  opnneir  49031  i0oii  49044  io1ii  49045