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  3676  dfss2  3920  eqbrrdva  5809  f1oiso2  7286  frxp  8056  onfununi  8261  smoel2  8283  smoiso2  8289  3ecoptocl  8733  ssfi  9082  f1domfi  9090  rex2dom  9137  fodomfib  9213  dffi2  9307  elfiun  9314  dif1card  9898  infxpenlem  9901  cfeq0  10144  cfsuc  10145  cfflb  10147  cfslb2n  10156  cofsmo  10157  domtriomlem  10330  axdc3lem4  10341  axdc4lem  10343  ttukey2g  10404  tskxpss  10660  grudomon  10705  elnpi  10876  dedekind  11273  nn0n0n1ge2b  12447  fzind  12568  suprzcl2  12833  icoshft  13370  fzen  13438  hashgt23el  14328  hashfundm  14346  hashbclem  14356  seqcoll  14368  relexpsucl  14935  relexpsucr  14936  relexpfld  14953  shftuz  14973  mulgcd  16456  algcvga  16487  lcmneg  16511  ressbas  17144  resseqnbas  17150  ressress  17155  psss  18483  tsrlemax  18489  isnmgm  18549  gsummgmpropd  18586  issgrpd  18635  iscmnd  19704  ring1ne0  20215  unitmulclb  20297  isdrngd  20678  isdrngdOLD  20680  abvn0b  20749  issrngd  20768  rmodislmodlem  20860  rmodislmod  20861  isphld  21589  mpfaddcl  22038  mpfmulcl  22039  pf1addcl  22266  pf1mulcl  22267  fitop  22813  hausnei2  23266  ordtt1  23292  locfincmp  23439  basqtop  23624  filfi  23772  fgcl  23791  neifil  23793  filuni  23798  cnextcn  23980  prdsmet  24283  blssps  24337  blss  24338  metcnp3  24453  hlhil  25368  volsup2  25531  sincosq1sgn  26432  sincosq2sgn  26433  sincosq3sgn  26434  sincosq4sgn  26435  sinq12ge0  26442  bcmono  27213  n0cutlt  28283  iswlkg  29590  umgrwwlks2on  29933  clwlkclwwlkfo  29984  3cyclfrgrrn1  30260  grpodivf  30513  ipf  30688  shintcli  31304  spanuni  31519  adjadj  31911  unopadj2  31913  hmopadj  31914  hmopbdoptHIL  31963  resvsca  33292  resvlem  33293  submateq  33817  esumcocn  34088  bnj1379  34837  bnj571  34913  bnj594  34919  bnj580  34920  bnj600  34926  bnj1189  35016  bnj1321  35034  bnj1384  35039  f1resrcmplf1dlem  35093  trssfir1omregs  35120  cplgredgex  35153  cusgr3cyclex  35168  loop1cycl  35169  umgr2cycllem  35172  umgr2cycl  35173  acycgr2v  35182  cusgracyclt3v  35188  climuzcnv  35703  fness  36382  bj-idreseq  37195  bj-imdiridlem  37218  neificl  37792  metf1o  37794  isismty  37840  ismtybndlem  37845  ablo4pnp  37919  divrngcl  37996  keridl  38071  prnc  38106  lsmsatcv  39048  llncvrlpln2  39595  lplncvrlvol2  39653  linepsubN  39790  pmapsub  39806  dalawlem10  39918  dalawlem13  39921  dalawlem14  39922  dalaw  39924  diaf11N  41087  dibf11N  41199  ismrcd1  42730  ismrcd2  42731  mzpincl  42766  mzpadd  42770  mzpmul  42771  pellfundge  42914  imasgim  43132  sqrtcval  43673  stoweidlem2  46039  stoweidlem17  46054  imaelsetpreimafv  47425  opnneir  48937  i0oii  48950  io1ii  48951