Theorem 3expib 1134

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  3anidm12  1437  mob  3679  dfss2  3922  eqbrrdva  5839  f1oiso2  7332  frxp  8101  onfununi  8307  smoel2  8329  smoiso2  8335  3ecoptocl  8786  ssfi  9137  f1domfi  9145  rex2dom  9193  fodomfib  9269  dffi2  9366  elfiun  9373  dif1card  9963  infxpenlem  9966  cfeq0  10210  cfsuc  10211  cfflb  10213  cfslb2n  10222  cofsmo  10223  domtriomlem  10396  axdc3lem4  10407  axdc4lem  10409  ttukey2g  10470  tskxpss  10727  grudomon  10772  elnpi  10943  dedekind  11343  nn0n0n1ge2b  12547  fzind  12668  suprzcl2  12936  icoshft  13474  fzen  13543  hashgt23el  14434  hashfundm  14452  hashbclem  14462  seqcoll  14474  relexpsucl  15041  relexpsucr  15042  relexpfld  15059  shftuz  15079  mulgcd  16565  algcvga  16596  lcmneg  16620  ressbas  17255  resseqnbas  17261  ressress  17266  psss  18595  tsrlemax  18601  isnmgm  18661  gsummgmpropd  18698  issgrpd  18747  iscmnd  19817  ring1ne0  20328  unitmulclb  20409  isdrngd  20794  isdrngdOLD  20796  abvn0b  20865  issrngd  20884  rmodislmodlem  20976  rmodislmod  20977  isphld  21686  mpfaddcl  22146  mpfmulcl  22147  pf1addcl  22396  pf1mulcl  22397  fitop  22940  hausnei2  23393  ordtt1  23419  locfincmp  23566  basqtop  23751  filfi  23899  fgcl  23918  neifil  23920  filuni  23925  cnextcn  24107  prdsmet  24410  blssps  24464  blss  24465  metcnp3  24580  hlhil  25485  volsup2  25647  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12ge0  26550  bcmono  27318  n0cutlt  28429  bdayfin  28557  iswlkg  29760  usgrwwlks2on  30104  umgrwwlks2on  30105  clwlkclwwlkfo  30157  3cyclfrgrrn1  30433  grpodivf  30687  ipf  30862  shintcli  31478  spanuni  31693  adjadj  32085  unopadj2  32087  hmopadj  32088  hmopbdoptHIL  32137  resvsca  33479  resvlem  33480  submateq  34067  esumcocn  34338  bnj1379  35089  bnj571  35165  bnj594  35171  bnj580  35172  bnj600  35178  bnj1189  35268  bnj1321  35286  bnj1384  35291  f1resrcmplf1dlem  35344  trssfir1om  35371  fineqvinfep  35385  trssfir1omregs  35396  onvfowev  35423  cplgredgex  35435  cusgr3cyclex  35450  loop1cycl  35451  umgr2cycllem  35454  umgr2cycl  35455  acycgr2v  35464  cusgracyclt3v  35470  climuzcnv  35985  fness  36673  cgsex2gd  37593  bj-idreseq  37618  bj-imdiridlem  37641  neificl  38216  metf1o  38218  isismty  38264  ismtybndlem  38269  ablo4pnp  38343  divrngcl  38420  keridl  38495  prnc  38530  lsmsatcv  39598  llncvrlpln2  40145  lplncvrlvol2  40203  linepsubN  40340  pmapsub  40356  dalawlem10  40468  dalawlem13  40471  dalawlem14  40472  dalaw  40474  diaf11N  41637  dibf11N  41749  ismrcd1  43243  ismrcd2  43244  mzpincl  43279  mzpadd  43283  mzpmul  43284  pellfundge  43423  imasgim  43641  sqrtcval  44181  stoweidlem2  46540  stoweidlem17  46555  imaelsetpreimafv  47965  opnneir  49492  i0oii  49505  io1ii  49506