Theorem 3expib 1140

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anidm12  1446  mob  3683  dfss2  3926  eqbrrdva  5860  f1resrcmplf1dlem  7279  f1oiso2  7361  frxp  8131  onfununi  8337  smoel2  8359  smoiso2  8365  3ecoptocl  8816  ssfi  9167  f1domfi  9175  rex2dom  9223  fodomfib  9298  dffi2  9393  elfiun  9400  dif1card  10013  infxpenlem  10016  cfeq0  10258  cfsuc  10259  cfflb  10261  cfslb2n  10270  cofsmo  10271  domtriomlem  10444  axdc3lem4  10455  axdc4lem  10457  ttukey2g  10518  tskxpss  10775  grudomon  10820  elnpi  10991  dedekind  11391  nn0n0n1ge2b  12591  fzind  12712  suprzcl2  12980  icoshft  13518  fzen  13587  hashgt23el  14481  hashfundm  14499  hashbclem  14509  seqcoll  14521  relexpsucl  15094  relexpsucr  15095  relexpfld  15112  shftuz  15132  mulgcd  16631  algcvga  16662  lcmneg  16686  ressbas  17321  resseqnbas  17327  ressress  17332  psss  18661  tsrlemax  18667  isnmgm  18727  gsummgmpropd  18768  issgrpd  18817  iscmnd  19895  ring1ne0  20415  unitmulclb  20496  isdrngd  20905  isdrngdOLD  20907  abvn0b  20976  issrngd  20995  rmodislmodlem  21087  rmodislmod  21088  isphld  21841  mpfaddcl  22301  mpfmulcl  22302  pf1addcl  22550  pf1mulcl  22551  fitop  23094  hausnei2  23547  ordtt1  23573  locfincmp  23720  basqtop  23905  filfi  24053  fgcl  24072  neifil  24074  filuni  24079  cnextcn  24261  prdsmet  24564  blssps  24618  blss  24619  metcnp3  24734  hlhil  25639  volsup2  25801  sincosq1sgn  26700  sincosq2sgn  26701  sincosq3sgn  26702  sincosq4sgn  26703  sinq12ge0  26710  bcmono  27478  n0cutlt  28589  bdayfin  28717  iswlkg  30000  usgrwwlks2on  30344  umgrwwlks2on  30345  clwlkclwwlkfo  30397  3cyclfrgrrn1  30673  grpodivf  30927  ipf  31102  shintcli  31718  spanuni  31933  adjadj  32325  unopadj2  32327  hmopadj  32328  hmopbdoptHIL  32377  resvsca  33683  resvlem  33684  submateq  34230  esumcocn  34501  bnj1379  35250  bnj571  35326  bnj594  35332  bnj580  35333  bnj600  35339  bnj1189  35429  bnj1321  35447  bnj1384  35452  trssfir1om  35532  fineqvinfep  35562  trssfir1omregs  35573  karddom  35598  kardsdom  35599  kardexen  35600  onvfowev  35624  cplgredgex  35634  cusgr3cyclex  35649  loop1cycl  35650  umgr2cycllem  35653  umgr2cycl  35654  acycgr2v  35663  cusgracyclt3v  35669  climuzcnv  36184  fness  36901  cgsex2gd  37822  bj-idreseq  37847  bj-imdiridlem  37870  neificl  38445  metf1o  38447  isismty  38493  ismtybndlem  38498  ablo4pnp  38572  divrngcl  38649  keridl  38724  prnc  38759  lsmsatcv  39825  llncvrlpln2  40372  lplncvrlvol2  40430  linepsubN  40567  pmapsub  40583  dalawlem10  40695  dalawlem13  40698  dalawlem14  40699  dalaw  40701  diaf11N  41864  dibf11N  41976  ismrcd1  43470  ismrcd2  43471  mzpincl  43506  mzpadd  43510  mzpmul  43511  pellfundge  43650  imasgim  43868  sqrtcval  44408  stoweidlem2  46757  stoweidlem17  46772  imaelsetpreimafv  48185  opnneir  49726  i0oii  49739  io1ii  49740