Theorem 3expib 1123

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anidm12  1421  mob  3723  dfss2  3969  eqbrrdva  5880  f1oiso2  7372  frxp  8151  onfununi  8381  smoel2  8403  smoiso2  8409  3ecoptocl  8849  ssfi  9213  f1domfi  9221  rex2dom  9282  fodomfib  9369  dffi2  9463  elfiun  9470  dif1card  10050  infxpenlem  10053  cfeq0  10296  cfsuc  10297  cfflb  10299  cfslb2n  10308  cofsmo  10309  domtriomlem  10482  axdc3lem4  10493  axdc4lem  10495  ttukey2g  10556  tskxpss  10812  grudomon  10857  elnpi  11028  dedekind  11424  nn0n0n1ge2b  12595  fzind  12716  suprzcl2  12980  icoshft  13513  fzen  13581  hashgt23el  14463  hashfundm  14481  hashbclem  14491  seqcoll  14503  relexpsucl  15070  relexpsucr  15071  relexpfld  15088  shftuz  15108  mulgcd  16585  algcvga  16616  lcmneg  16640  ressbas  17280  ressbasOLD  17281  resseqnbas  17287  resslemOLD  17288  ressress  17293  psss  18625  tsrlemax  18631  isnmgm  18657  gsummgmpropd  18694  issgrpd  18743  iscmnd  19812  ring1ne0  20296  unitmulclb  20381  isdrngd  20765  isdrngdOLD  20767  abvn0b  20837  issrngd  20856  rmodislmodlem  20927  rmodislmod  20928  isphld  21672  mpfaddcl  22129  mpfmulcl  22130  pf1addcl  22357  pf1mulcl  22358  fitop  22906  hausnei2  23361  ordtt1  23387  locfincmp  23534  basqtop  23719  filfi  23867  fgcl  23886  neifil  23888  filuni  23893  cnextcn  24075  prdsmet  24380  blssps  24434  blss  24435  metcnp3  24553  hlhil  25477  volsup2  25640  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12ge0  26550  bcmono  27321  iswlkg  29631  umgrwwlks2on  29977  clwlkclwwlkfo  30028  3cyclfrgrrn1  30304  grpodivf  30557  ipf  30732  shintcli  31348  spanuni  31563  adjadj  31955  unopadj2  31957  hmopadj  31958  hmopbdoptHIL  32007  resvsca  33356  resvlem  33357  resvlemOLD  33358  submateq  33808  esumcocn  34081  bnj1379  34844  bnj571  34920  bnj594  34926  bnj580  34927  bnj600  34933  bnj1189  35023  bnj1321  35041  bnj1384  35046  f1resrcmplf1dlem  35100  cplgredgex  35126  cusgr3cyclex  35141  loop1cycl  35142  umgr2cycllem  35145  umgr2cycl  35146  acycgr2v  35155  cusgracyclt3v  35161  climuzcnv  35676  fness  36350  bj-idreseq  37163  bj-imdiridlem  37186  neificl  37760  metf1o  37762  isismty  37808  ismtybndlem  37813  ablo4pnp  37887  divrngcl  37964  keridl  38039  prnc  38074  lsmsatcv  39011  llncvrlpln2  39559  lplncvrlvol2  39617  linepsubN  39754  pmapsub  39770  dalawlem10  39882  dalawlem13  39885  dalawlem14  39886  dalaw  39888  diaf11N  41051  dibf11N  41163  ismrcd1  42709  ismrcd2  42710  mzpincl  42745  mzpadd  42749  mzpmul  42750  pellfundge  42893  imasgim  43112  sqrtcval  43654  stoweidlem2  46017  stoweidlem17  46032  imaelsetpreimafv  47382  opnneir  48804  i0oii  48817  io1ii  48818