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  3674  dfss2  4094  eqbrrdva  5846  f1resrcmplf1dlem  7278  f1oiso2  7360  frxp  8140  onfununi  8352  smoel2  8374  smoiso2  8380  3ecoptocl  8833  ssfi  9191  f1domfi  9199  rex2dom  9247  fodomfib  9323  dffi2  9418  elfiun  9425  dif1card  10092  infxpenlem  10095  cfeq0  10337  cfsuc  10338  cfflb  10340  cfslb2n  10349  cofsmo  10350  domtriomlem  10523  axdc3lem4  10534  axdc4lem  10536  ttukey2g  10597  tskxpss  10860  grudomon  10905  elnpi  11076  dedekind  11476  nn0n0n1ge2b  12678  fzind  12800  suprzcl2  13068  icoshft  13607  fzen  13677  hashgt23el  14572  hashfundm  14590  hashbclem  14600  seqcoll  14612  relexpsucl  15189  relexpsucr  15190  relexpfld  15207  shftuz  15227  mulgcd  16726  algcvga  16759  lcmneg  16783  ressbas  17419  resseqnbas  17425  ressress  17430  psss  18759  tsrlemax  18765  isnmgm  18825  gsummgmpropd  18875  issgrpd  18924  iscmnd  20013  ring1ne0  20535  unitmulclb  20616  isdrngd  21027  isdrngdOLD  21029  abvn0b  21098  issrngd  21117  rmodislmodlem  21209  rmodislmod  21210  isphld  21965  mpfaddcl  22427  mpfmulcl  22428  pf1addcl  22676  pf1mulcl  22677  fitop  23223  hausnei2  23676  ordtt1  23702  locfincmp  23850  basqtop  24035  filfi  24183  fgcl  24202  neifil  24204  filuni  24209  cnextcn  24391  prdsmet  24694  blssps  24748  blss  24749  metcnp3  24864  hlhil  25769  volsup2  25931  sincosq1sgn  26832  sincosq2sgn  26833  sincosq3sgn  26834  sincosq4sgn  26835  sinq12ge0  26842  bcmono  27609  n0cutlt  28750  bdayfin  28878  iswlkg  30199  usgrwwlks2on  30552  umgrwwlks2on  30553  clwlkclwwlkfo  30605  loop1cycl  30749  umgr2cycllem  30751  umgr2cycl  30752  3cyclfrgrrn1  30891  grpodivf  31145  ipf  31320  shintcli  31936  spanuni  32151  adjadj  32543  unopadj2  32545  hmopadj  32546  hmopbdoptHIL  32595  resvsca  33939  resvlem  33940  submateq  34487  esumcocn  34758  bnj1379  35506  bnj571  35582  bnj594  35588  bnj580  35589  bnj600  35595  bnj1189  35685  bnj1321  35703  bnj1384  35708  trssfir1om  35789  fineqvinfep  35849  trssfir1omregs  35860  karddom  35885  kardsdom  35886  kardexen  35887  onprcf1acwevdlem1  35964  onvfowev  35969  cplgredgex  35981  cusgr3cyclex  35987  acycgr2v  35991  cusgracyclt3v  35997  climuzcnv  36522  fness  37229  cgsex2gd  38151  bj-idreseq  38176  bj-imdiridlem  38199  neificl  38780  metf1o  38782  isismty  38828  ismtybndlem  38833  ablo4pnp  38907  divrngcl  38984  keridl  39059  prnc  39094  lsmsatcv  40160  llncvrlpln2  40707  lplncvrlvol2  40765  linepsubN  40902  pmapsub  40918  dalawlem10  41030  dalawlem13  41033  dalawlem14  41034  dalaw  41036  diaf11N  42199  dibf11N  42311  ismrcd1  43802  ismrcd2  43803  mzpincl  43838  mzpadd  43842  mzpmul  43843  pellfundge  43982  imasgim  44195  sqrtcval  44734  stoweidlem2  47105  stoweidlem17  47120  imaelsetpreimafv  48570  opnneir  50114  i0oii  50127  io1ii  50128