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  3675  dfss2  3917  eqbrrdva  5847  f1resrcmplf1dlem  7270  f1oiso2  7352  frxp  8127  onfununi  8333  smoel2  8355  smoiso2  8361  3ecoptocl  8814  ssfi  9172  f1domfi  9180  rex2dom  9228  fodomfib  9304  dffi2  9399  elfiun  9406  dif1card  10070  infxpenlem  10073  cfeq0  10315  cfsuc  10316  cfflb  10318  cfslb2n  10327  cofsmo  10328  domtriomlem  10501  axdc3lem4  10512  axdc4lem  10514  ttukey2g  10575  tskxpss  10838  grudomon  10883  elnpi  11054  dedekind  11454  nn0n0n1ge2b  12656  fzind  12778  suprzcl2  13046  icoshft  13585  fzen  13654  hashgt23el  14549  hashfundm  14567  hashbclem  14577  seqcoll  14589  relexpsucl  15164  relexpsucr  15165  relexpfld  15182  shftuz  15202  mulgcd  16701  algcvga  16734  lcmneg  16758  ressbas  17394  resseqnbas  17400  ressress  17405  psss  18734  tsrlemax  18740  isnmgm  18800  gsummgmpropd  18850  issgrpd  18899  iscmnd  19988  ring1ne0  20510  unitmulclb  20591  isdrngd  21002  isdrngdOLD  21004  abvn0b  21073  issrngd  21092  rmodislmodlem  21184  rmodislmod  21185  isphld  21940  mpfaddcl  22402  mpfmulcl  22403  pf1addcl  22651  pf1mulcl  22652  fitop  23198  hausnei2  23651  ordtt1  23677  locfincmp  23825  basqtop  24010  filfi  24158  fgcl  24177  neifil  24179  filuni  24184  cnextcn  24366  prdsmet  24669  blssps  24723  blss  24724  metcnp3  24839  hlhil  25744  volsup2  25906  sincosq1sgn  26809  sincosq2sgn  26810  sincosq3sgn  26811  sincosq4sgn  26812  sinq12ge0  26819  bcmono  27586  n0cutlt  28727  bdayfin  28855  iswlkg  30176  usgrwwlks2on  30529  umgrwwlks2on  30530  clwlkclwwlkfo  30582  loop1cycl  30726  umgr2cycllem  30728  umgr2cycl  30729  3cyclfrgrrn1  30868  grpodivf  31122  ipf  31297  shintcli  31913  spanuni  32128  adjadj  32520  unopadj2  32522  hmopadj  32523  hmopbdoptHIL  32572  resvsca  33875  resvlem  33876  submateq  34423  esumcocn  34694  bnj1379  35443  bnj571  35519  bnj594  35525  bnj580  35526  bnj600  35532  bnj1189  35622  bnj1321  35640  bnj1384  35645  trssfir1om  35716  fineqvinfep  35766  trssfir1omregs  35777  karddom  35802  kardsdom  35803  kardexen  35804  onvfowev  35868  cplgredgex  35874  cusgr3cyclex  35880  acycgr2v  35884  cusgracyclt3v  35890  climuzcnv  36405  fness  37107  cgsex2gd  38026  bj-idreseq  38051  bj-imdiridlem  38074  neificl  38655  metf1o  38657  isismty  38703  ismtybndlem  38708  ablo4pnp  38782  divrngcl  38859  keridl  38934  prnc  38969  lsmsatcv  40035  llncvrlpln2  40582  lplncvrlvol2  40640  linepsubN  40777  pmapsub  40793  dalawlem10  40905  dalawlem13  40908  dalawlem14  40909  dalaw  40911  diaf11N  42074  dibf11N  42186  ismrcd1  43662  ismrcd2  43663  mzpincl  43698  mzpadd  43702  mzpmul  43703  pellfundge  43842  imasgim  44060  sqrtcval  44600  stoweidlem2  46956  stoweidlem17  46971  imaelsetpreimafv  48421  opnneir  49959  i0oii  49972  io1ii  49973