Theorem 3expib 1117

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3anidm12  1530  mob  3529  eqbrrdva  5447  fco  6219  f1oiso2  6766  frxp  7456  onfununi  7608  smoel2  7630  smoiso2  7636  3ecoptocl  8008  dffi2  8496  elfiun  8503  dif1card  9043  infxpenlem  9046  cfeq0  9290  cfsuc  9291  cfflb  9293  cfslb2n  9302  cofsmo  9303  domtriomlem  9476  axdc3lem4  9487  axdc4lem  9489  ttukey2g  9550  tskxpss  9806  grudomon  9851  elnpi  10022  dedekind  10412  nn0n0n1ge2b  11571  fzind  11687  suprzcl2  11991  icoshft  12507  fzen  12571  hashbclem  13448  seqcoll  13460  relexpsucr  13988  relexpsucl  13992  relexpfld  14008  shftuz  14028  mulgcd  15487  algcvga  15514  lcmneg  15538  ressbas  16152  resslem  16155  ressress  16160  psss  17435  tsrlemax  17441  isnmgm  17467  gsummgmpropd  17496  iscmnd  18425  ring1ne0  18811  unitmulclb  18885  isdrngd  18994  issrngd  19083  rmodislmodlem  19152  rmodislmod  19153  abvn0b  19524  mpfaddcl  19756  mpfmulcl  19757  pf1addcl  19939  pf1mulcl  19940  isphld  20221  fitop  20927  hausnei2  21379  ordtt1  21405  locfincmp  21551  basqtop  21736  filfi  21884  fgcl  21903  neifil  21905  filuni  21910  cnextcn  22092  prdsmet  22396  blssps  22450  blss  22451  metcnp3  22566  hlhil  23434  volsup2  23593  sincosq1sgn  24470  sincosq2sgn  24471  sincosq3sgn  24472  sincosq4sgn  24473  sinq12ge0  24480  bcmono  25222  iswlkg  26740  umgrwwlks2on  27099  clwlkclwwlkfo  27153  3cyclfrgrrn1  27460  grpodivf  27722  ipf  27898  shintcli  28518  spanuni  28733  adjadj  29125  unopadj2  29127  hmopadj  29128  hmopbdoptHIL  29177  resvsca  30160  resvlem  30161  submateq  30205  esumcocn  30472  bnj1379  31229  bnj571  31304  bnj594  31310  bnj580  31311  bnj600  31317  bnj1189  31405  bnj1321  31423  bnj1384  31428  climuzcnv  31893  fness  32671  neificl  33880  metf1o  33882  isismty  33931  ismtybndlem  33936  ablo4pnp  34010  divrngcl  34087  keridl  34162  prnc  34197  lsmsatcv  34818  llncvrlpln2  35364  lplncvrlvol2  35422  linepsubN  35559  pmapsub  35575  dalawlem10  35687  dalawlem13  35690  dalawlem14  35691  dalaw  35693  diaf11N  36858  dibf11N  36970  ismrcd1  37781  ismrcd2  37782  mzpincl  37817  mzpadd  37821  mzpmul  37822  pellfundge  37966  imasgim  38190  stoweidlem2  40740  stoweidlem17  40755