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  3688  dfss2  3932  eqbrrdva  5833  f1oiso2  7327  frxp  8105  onfununi  8310  smoel2  8332  smoiso2  8338  3ecoptocl  8782  ssfi  9137  f1domfi  9145  rex2dom  9193  fodomfib  9280  dffi2  9374  elfiun  9381  dif1card  9963  infxpenlem  9966  cfeq0  10209  cfsuc  10210  cfflb  10212  cfslb2n  10221  cofsmo  10222  domtriomlem  10395  axdc3lem4  10406  axdc4lem  10408  ttukey2g  10469  tskxpss  10725  grudomon  10770  elnpi  10941  dedekind  11337  nn0n0n1ge2b  12511  fzind  12632  suprzcl2  12897  icoshft  13434  fzen  13502  hashgt23el  14389  hashfundm  14407  hashbclem  14417  seqcoll  14429  relexpsucl  14997  relexpsucr  14998  relexpfld  15015  shftuz  15035  mulgcd  16518  algcvga  16549  lcmneg  16573  ressbas  17206  resseqnbas  17212  ressress  17217  psss  18539  tsrlemax  18545  isnmgm  18571  gsummgmpropd  18608  issgrpd  18657  iscmnd  19724  ring1ne0  20208  unitmulclb  20290  isdrngd  20674  isdrngdOLD  20676  abvn0b  20745  issrngd  20764  rmodislmodlem  20835  rmodislmod  20836  isphld  21563  mpfaddcl  22012  mpfmulcl  22013  pf1addcl  22240  pf1mulcl  22241  fitop  22787  hausnei2  23240  ordtt1  23266  locfincmp  23413  basqtop  23598  filfi  23746  fgcl  23765  neifil  23767  filuni  23772  cnextcn  23954  prdsmet  24258  blssps  24312  blss  24313  metcnp3  24428  hlhil  25343  volsup2  25506  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  sinq12ge0  26417  bcmono  27188  n0cutlt  28249  iswlkg  29541  umgrwwlks2on  29887  clwlkclwwlkfo  29938  3cyclfrgrrn1  30214  grpodivf  30467  ipf  30642  shintcli  31258  spanuni  31473  adjadj  31865  unopadj2  31867  hmopadj  31868  hmopbdoptHIL  31917  resvsca  33304  resvlem  33305  submateq  33799  esumcocn  34070  bnj1379  34820  bnj571  34896  bnj594  34902  bnj580  34903  bnj600  34909  bnj1189  34999  bnj1321  35017  bnj1384  35022  f1resrcmplf1dlem  35076  cplgredgex  35108  cusgr3cyclex  35123  loop1cycl  35124  umgr2cycllem  35127  umgr2cycl  35128  acycgr2v  35137  cusgracyclt3v  35143  climuzcnv  35658  fness  36337  bj-idreseq  37150  bj-imdiridlem  37173  neificl  37747  metf1o  37749  isismty  37795  ismtybndlem  37800  ablo4pnp  37874  divrngcl  37951  keridl  38026  prnc  38061  lsmsatcv  39003  llncvrlpln2  39551  lplncvrlvol2  39609  linepsubN  39746  pmapsub  39762  dalawlem10  39874  dalawlem13  39877  dalawlem14  39878  dalaw  39880  diaf11N  41043  dibf11N  41155  ismrcd1  42686  ismrcd2  42687  mzpincl  42722  mzpadd  42726  mzpmul  42727  pellfundge  42870  imasgim  43089  sqrtcval  43630  stoweidlem2  46000  stoweidlem17  46015  imaelsetpreimafv  47396  opnneir  48895  i0oii  48908  io1ii  48909