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 415	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anidm12  1446  mob  3681  dfss2  3924  eqbrrdva  5857  f1oiso2  7352  frxp  8123  onfununi  8329  smoel2  8351  smoiso2  8357  3ecoptocl  8808  ssfi  9158  f1domfi  9166  rex2dom  9214  fodomfib  9289  dffi2  9384  elfiun  9391  dif1card  9995  infxpenlem  9998  cfeq0  10241  cfsuc  10242  cfflb  10244  cfslb2n  10253  cofsmo  10254  domtriomlem  10427  axdc3lem4  10438  axdc4lem  10440  ttukey2g  10501  tskxpss  10758  grudomon  10803  elnpi  10974  dedekind  11374  nn0n0n1ge2b  12574  fzind  12695  suprzcl2  12963  icoshft  13501  fzen  13570  hashgt23el  14463  hashfundm  14481  hashbclem  14491  seqcoll  14503  relexpsucl  15070  relexpsucr  15071  relexpfld  15088  shftuz  15108  mulgcd  16607  algcvga  16638  lcmneg  16662  ressbas  17297  resseqnbas  17303  ressress  17308  psss  18637  tsrlemax  18643  isnmgm  18703  gsummgmpropd  18740  issgrpd  18789  iscmnd  19865  ring1ne0  20383  unitmulclb  20464  isdrngd  20850  isdrngdOLD  20852  abvn0b  20920  issrngd  20939  rmodislmodlem  21031  rmodislmod  21032  isphld  21785  mpfaddcl  22245  mpfmulcl  22246  pf1addcl  22494  pf1mulcl  22495  fitop  23038  hausnei2  23491  ordtt1  23517  locfincmp  23664  basqtop  23849  filfi  23997  fgcl  24016  neifil  24018  filuni  24023  cnextcn  24205  prdsmet  24508  blssps  24562  blss  24563  metcnp3  24678  hlhil  25583  volsup2  25745  sincosq1sgn  26644  sincosq2sgn  26645  sincosq3sgn  26646  sincosq4sgn  26647  sinq12ge0  26654  bcmono  27422  n0cutlt  28533  bdayfin  28661  iswlkg  29944  usgrwwlks2on  30288  umgrwwlks2on  30289  clwlkclwwlkfo  30341  3cyclfrgrrn1  30617  grpodivf  30871  ipf  31046  shintcli  31662  spanuni  31877  adjadj  32269  unopadj2  32271  hmopadj  32272  hmopbdoptHIL  32321  resvsca  33633  resvlem  33634  submateq  34180  esumcocn  34451  bnj1379  35199  bnj571  35275  bnj594  35281  bnj580  35282  bnj600  35288  bnj1189  35378  bnj1321  35396  bnj1384  35401  f1resrcmplf1dlem  35455  trssfir1om  35488  fineqvinfep  35519  trssfir1omregs  35530  karddom  35555  kardsdom  35556  kardexen  35557  onvfowev  35581  cplgredgex  35594  cusgr3cyclex  35609  loop1cycl  35610  umgr2cycllem  35613  umgr2cycl  35614  acycgr2v  35623  cusgracyclt3v  35629  climuzcnv  36144  fness  36841  cgsex2gd  37762  bj-idreseq  37787  bj-imdiridlem  37810  neificl  38385  metf1o  38387  isismty  38433  ismtybndlem  38438  ablo4pnp  38512  divrngcl  38589  keridl  38664  prnc  38699  lsmsatcv  39765  llncvrlpln2  40312  lplncvrlvol2  40370  linepsubN  40507  pmapsub  40523  dalawlem10  40635  dalawlem13  40638  dalawlem14  40639  dalaw  40641  diaf11N  41804  dibf11N  41916  ismrcd1  43412  ismrcd2  43413  mzpincl  43448  mzpadd  43452  mzpmul  43453  pellfundge  43592  imasgim  43810  sqrtcval  44350  stoweidlem2  46699  stoweidlem17  46714  imaelsetpreimafv  48127  opnneir  49668  i0oii  49681  io1ii  49682