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  3679  dfss2  3923  eqbrrdva  5816  f1oiso2  7293  frxp  8066  onfununi  8271  smoel2  8293  smoiso2  8299  3ecoptocl  8743  ssfi  9097  f1domfi  9105  rex2dom  9152  fodomfib  9238  dffi2  9332  elfiun  9339  dif1card  9923  infxpenlem  9926  cfeq0  10169  cfsuc  10170  cfflb  10172  cfslb2n  10181  cofsmo  10182  domtriomlem  10355  axdc3lem4  10366  axdc4lem  10368  ttukey2g  10429  tskxpss  10685  grudomon  10730  elnpi  10901  dedekind  11297  nn0n0n1ge2b  12471  fzind  12592  suprzcl2  12857  icoshft  13394  fzen  13462  hashgt23el  14349  hashfundm  14367  hashbclem  14377  seqcoll  14389  relexpsucl  14956  relexpsucr  14957  relexpfld  14974  shftuz  14994  mulgcd  16477  algcvga  16508  lcmneg  16532  ressbas  17165  resseqnbas  17171  ressress  17176  psss  18504  tsrlemax  18510  isnmgm  18536  gsummgmpropd  18573  issgrpd  18622  iscmnd  19691  ring1ne0  20202  unitmulclb  20284  isdrngd  20668  isdrngdOLD  20670  abvn0b  20739  issrngd  20758  rmodislmodlem  20850  rmodislmod  20851  isphld  21579  mpfaddcl  22028  mpfmulcl  22029  pf1addcl  22256  pf1mulcl  22257  fitop  22803  hausnei2  23256  ordtt1  23282  locfincmp  23429  basqtop  23614  filfi  23762  fgcl  23781  neifil  23783  filuni  23788  cnextcn  23970  prdsmet  24274  blssps  24328  blss  24329  metcnp3  24444  hlhil  25359  volsup2  25522  sincosq1sgn  26423  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  sinq12ge0  26433  bcmono  27204  n0cutlt  28272  iswlkg  29577  umgrwwlks2on  29920  clwlkclwwlkfo  29971  3cyclfrgrrn1  30247  grpodivf  30500  ipf  30675  shintcli  31291  spanuni  31506  adjadj  31898  unopadj2  31900  hmopadj  31901  hmopbdoptHIL  31950  resvsca  33280  resvlem  33281  submateq  33775  esumcocn  34046  bnj1379  34796  bnj571  34872  bnj594  34878  bnj580  34879  bnj600  34885  bnj1189  34975  bnj1321  34993  bnj1384  34998  f1resrcmplf1dlem  35052  cplgredgex  35093  cusgr3cyclex  35108  loop1cycl  35109  umgr2cycllem  35112  umgr2cycl  35113  acycgr2v  35122  cusgracyclt3v  35128  climuzcnv  35643  fness  36322  bj-idreseq  37135  bj-imdiridlem  37158  neificl  37732  metf1o  37734  isismty  37780  ismtybndlem  37785  ablo4pnp  37859  divrngcl  37936  keridl  38011  prnc  38046  lsmsatcv  38988  llncvrlpln2  39536  lplncvrlvol2  39594  linepsubN  39731  pmapsub  39747  dalawlem10  39859  dalawlem13  39862  dalawlem14  39863  dalaw  39865  diaf11N  41028  dibf11N  41140  ismrcd1  42671  ismrcd2  42672  mzpincl  42707  mzpadd  42711  mzpmul  42712  pellfundge  42855  imasgim  43073  sqrtcval  43614  stoweidlem2  45984  stoweidlem17  45999  imaelsetpreimafv  47380  opnneir  48892  i0oii  48905  io1ii  48906