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 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  1419  mob  3739  dfss2  3994  eqbrrdva  5894  fcoOLD  6772  f1oiso2  7388  frxp  8167  onfununi  8397  smoel2  8419  smoiso2  8425  3ecoptocl  8867  ssfi  9240  f1domfi  9247  rex2dom  9309  fodomfib  9397  dffi2  9492  elfiun  9499  dif1card  10079  infxpenlem  10082  cfeq0  10325  cfsuc  10326  cfflb  10328  cfslb2n  10337  cofsmo  10338  domtriomlem  10511  axdc3lem4  10522  axdc4lem  10524  ttukey2g  10585  tskxpss  10841  grudomon  10886  elnpi  11057  dedekind  11453  nn0n0n1ge2b  12621  fzind  12741  suprzcl2  13003  icoshft  13533  fzen  13601  hashgt23el  14473  hashfundm  14491  hashbclem  14501  seqcoll  14513  relexpsucl  15080  relexpsucr  15081  relexpfld  15098  shftuz  15118  mulgcd  16595  algcvga  16626  lcmneg  16650  ressbas  17293  ressbasOLD  17294  resseqnbas  17300  resslemOLD  17301  ressress  17307  psss  18650  tsrlemax  18656  isnmgm  18682  gsummgmpropd  18719  issgrpd  18768  iscmnd  19836  ring1ne0  20322  unitmulclb  20407  isdrngd  20787  isdrngdOLD  20789  abvn0b  20859  issrngd  20878  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  isphld  21695  mpfaddcl  22152  mpfmulcl  22153  pf1addcl  22378  pf1mulcl  22379  fitop  22927  hausnei2  23382  ordtt1  23408  locfincmp  23555  basqtop  23740  filfi  23888  fgcl  23907  neifil  23909  filuni  23914  cnextcn  24096  prdsmet  24401  blssps  24455  blss  24456  metcnp3  24574  hlhil  25496  volsup2  25659  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  sinq12ge0  26568  bcmono  27339  iswlkg  29649  umgrwwlks2on  29990  clwlkclwwlkfo  30041  3cyclfrgrrn1  30317  grpodivf  30570  ipf  30745  shintcli  31361  spanuni  31576  adjadj  31968  unopadj2  31970  hmopadj  31971  hmopbdoptHIL  32020  resvsca  33321  resvlem  33322  resvlemOLD  33323  submateq  33755  esumcocn  34044  bnj1379  34806  bnj571  34882  bnj594  34888  bnj580  34889  bnj600  34895  bnj1189  34985  bnj1321  35003  bnj1384  35008  f1resrcmplf1dlem  35062  cplgredgex  35088  cusgr3cyclex  35104  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  acycgr2v  35118  cusgracyclt3v  35124  climuzcnv  35639  fness  36315  bj-idreseq  37128  bj-imdiridlem  37151  neificl  37713  metf1o  37715  isismty  37761  ismtybndlem  37766  ablo4pnp  37840  divrngcl  37917  keridl  37992  prnc  38027  lsmsatcv  38966  llncvrlpln2  39514  lplncvrlvol2  39572  linepsubN  39709  pmapsub  39725  dalawlem10  39837  dalawlem13  39840  dalawlem14  39841  dalaw  39843  diaf11N  41006  dibf11N  41118  ismrcd1  42654  ismrcd2  42655  mzpincl  42690  mzpadd  42694  mzpmul  42695  pellfundge  42838  imasgim  43057  sqrtcval  43603  stoweidlem2  45923  stoweidlem17  45938  imaelsetpreimafv  47269  opnneir  48586  i0oii  48599  io1ii  48600