Theorem 3expib 1138

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anidm12  1442  mob  3683  dfss2  3925  eqbrrdva  5846  f1oiso2  7340  frxp  8110  onfununi  8316  smoel2  8338  smoiso2  8344  3ecoptocl  8795  ssfi  9145  f1domfi  9153  rex2dom  9201  fodomfib  9276  dffi2  9371  elfiun  9378  dif1card  9982  infxpenlem  9985  cfeq0  10228  cfsuc  10229  cfflb  10231  cfslb2n  10240  cofsmo  10241  domtriomlem  10414  axdc3lem4  10425  axdc4lem  10427  ttukey2g  10488  tskxpss  10745  grudomon  10790  elnpi  10961  dedekind  11361  nn0n0n1ge2b  12564  fzind  12685  suprzcl2  12953  icoshft  13491  fzen  13560  hashgt23el  14451  hashfundm  14469  hashbclem  14479  seqcoll  14491  relexpsucl  15058  relexpsucr  15059  relexpfld  15076  shftuz  15096  mulgcd  16596  algcvga  16627  lcmneg  16651  ressbas  17286  resseqnbas  17292  ressress  17297  psss  18626  tsrlemax  18632  isnmgm  18692  gsummgmpropd  18729  issgrpd  18778  iscmnd  19855  ring1ne0  20373  unitmulclb  20454  isdrngd  20838  isdrngdOLD  20840  abvn0b  20908  issrngd  20927  rmodislmodlem  21019  rmodislmod  21020  isphld  21764  mpfaddcl  22224  mpfmulcl  22225  pf1addcl  22474  pf1mulcl  22475  fitop  23018  hausnei2  23471  ordtt1  23497  locfincmp  23644  basqtop  23829  filfi  23977  fgcl  23996  neifil  23998  filuni  24003  cnextcn  24185  prdsmet  24488  blssps  24542  blss  24543  metcnp3  24658  hlhil  25563  volsup2  25725  sincosq1sgn  26621  sincosq2sgn  26622  sincosq3sgn  26623  sincosq4sgn  26624  sinq12ge0  26631  bcmono  27399  n0cutlt  28510  bdayfin  28638  iswlkg  29872  usgrwwlks2on  30216  umgrwwlks2on  30217  clwlkclwwlkfo  30269  3cyclfrgrrn1  30545  grpodivf  30799  ipf  30974  shintcli  31590  spanuni  31805  adjadj  32197  unopadj2  32199  hmopadj  32200  hmopbdoptHIL  32249  resvsca  33567  resvlem  33568  submateq  34116  esumcocn  34387  bnj1379  35135  bnj571  35211  bnj594  35217  bnj580  35218  bnj600  35224  bnj1189  35314  bnj1321  35332  bnj1384  35337  f1resrcmplf1dlem  35390  trssfir1om  35419  fineqvinfep  35433  trssfir1omregs  35444  onvfowev  35471  cplgredgex  35484  cusgr3cyclex  35499  loop1cycl  35500  umgr2cycllem  35503  umgr2cycl  35504  acycgr2v  35513  cusgracyclt3v  35519  climuzcnv  36034  fness  36722  cgsex2gd  37641  bj-idreseq  37666  bj-imdiridlem  37689  neificl  38264  metf1o  38266  isismty  38312  ismtybndlem  38317  ablo4pnp  38391  divrngcl  38468  keridl  38543  prnc  38578  lsmsatcv  39646  llncvrlpln2  40193  lplncvrlvol2  40251  linepsubN  40388  pmapsub  40404  dalawlem10  40516  dalawlem13  40519  dalawlem14  40520  dalaw  40522  diaf11N  41685  dibf11N  41797  ismrcd1  43291  ismrcd2  43292  mzpincl  43327  mzpadd  43331  mzpmul  43332  pellfundge  43471  imasgim  43689  sqrtcval  44229  stoweidlem2  46574  stoweidlem17  46589  imaelsetpreimafv  47999  opnneir  49536  i0oii  49549  io1ii  49550