Theorem 3expib 1123

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

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

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 1089

This theorem is referenced by:  3anidm12  1422  mob  3663  dfss2  3907  eqbrrdva  5824  f1oiso2  7307  frxp  8076  onfununi  8281  smoel2  8303  smoiso2  8309  3ecoptocl  8756  ssfi  9107  f1domfi  9115  rex2dom  9163  fodomfib  9239  dffi2  9336  elfiun  9343  dif1card  9932  infxpenlem  9935  cfeq0  10178  cfsuc  10179  cfflb  10181  cfslb2n  10190  cofsmo  10191  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  ttukey2g  10438  tskxpss  10695  grudomon  10740  elnpi  10911  dedekind  11309  nn0n0n1ge2b  12506  fzind  12627  suprzcl2  12888  icoshft  13426  fzen  13495  hashgt23el  14386  hashfundm  14404  hashbclem  14414  seqcoll  14426  relexpsucl  14993  relexpsucr  14994  relexpfld  15011  shftuz  15031  mulgcd  16517  algcvga  16548  lcmneg  16572  ressbas  17206  resseqnbas  17212  ressress  17217  psss  18546  tsrlemax  18552  isnmgm  18612  gsummgmpropd  18649  issgrpd  18698  iscmnd  19769  ring1ne0  20280  unitmulclb  20361  isdrngd  20742  isdrngdOLD  20744  abvn0b  20813  issrngd  20832  rmodislmodlem  20924  rmodislmod  20925  isphld  21634  mpfaddcl  22091  mpfmulcl  22092  pf1addcl  22318  pf1mulcl  22319  fitop  22865  hausnei2  23318  ordtt1  23344  locfincmp  23491  basqtop  23676  filfi  23824  fgcl  23843  neifil  23845  filuni  23850  cnextcn  24032  prdsmet  24335  blssps  24389  blss  24390  metcnp3  24505  hlhil  25410  volsup2  25572  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  sinq12ge0  26472  bcmono  27240  n0cutlt  28351  bdayfin  28479  iswlkg  29682  usgrwwlks2on  30026  umgrwwlks2on  30027  clwlkclwwlkfo  30079  3cyclfrgrrn1  30355  grpodivf  30609  ipf  30784  shintcli  31400  spanuni  31615  adjadj  32007  unopadj2  32009  hmopadj  32010  hmopbdoptHIL  32059  resvsca  33392  resvlem  33393  submateq  33953  esumcocn  34224  bnj1379  34972  bnj571  35048  bnj594  35054  bnj580  35055  bnj600  35061  bnj1189  35151  bnj1321  35169  bnj1384  35174  f1resrcmplf1dlem  35229  trssfir1om  35255  fineqvinfep  35269  trssfir1omregs  35280  cplgredgex  35303  cusgr3cyclex  35318  loop1cycl  35319  umgr2cycllem  35322  umgr2cycl  35323  acycgr2v  35332  cusgracyclt3v  35338  climuzcnv  35853  fness  36531  cgsex2gd  37451  bj-idreseq  37476  bj-imdiridlem  37499  neificl  38074  metf1o  38076  isismty  38122  ismtybndlem  38127  ablo4pnp  38201  divrngcl  38278  keridl  38353  prnc  38388  lsmsatcv  39456  llncvrlpln2  40003  lplncvrlvol2  40061  linepsubN  40198  pmapsub  40214  dalawlem10  40326  dalawlem13  40329  dalawlem14  40330  dalaw  40332  diaf11N  41495  dibf11N  41607  ismrcd1  43130  ismrcd2  43131  mzpincl  43166  mzpadd  43170  mzpmul  43171  pellfundge  43310  imasgim  43528  sqrtcval  44068  stoweidlem2  46430  stoweidlem17  46445  imaelsetpreimafv  47855  opnneir  49382  i0oii  49395  io1ii  49396