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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  3anidm12  1419  mob  3657  eqbrrdva  5791  fcoOLD  6655  f1oiso2  7255  frxp  7998  onfununi  8203  smoel2  8225  smoiso2  8231  3ecoptocl  8629  ssfi  8994  f1domfi  9005  rex2dom  9067  dffi2  9226  elfiun  9233  dif1card  9812  infxpenlem  9815  cfeq0  10058  cfsuc  10059  cfflb  10061  cfslb2n  10070  cofsmo  10071  domtriomlem  10244  axdc3lem4  10255  axdc4lem  10257  ttukey2g  10318  tskxpss  10574  grudomon  10619  elnpi  10790  dedekind  11184  nn0n0n1ge2b  12347  fzind  12464  suprzcl2  12724  icoshft  13251  fzen  13319  hashgt23el  14184  hashbclem  14209  seqcoll  14223  relexpsucl  14787  relexpsucr  14788  relexpfld  14805  shftuz  14825  mulgcd  16301  algcvga  16329  lcmneg  16353  ressbas  16992  ressbasOLD  16993  resseqnbas  16996  resslemOLD  16997  ressress  17003  psss  18343  tsrlemax  18349  isnmgm  18375  gsummgmpropd  18410  iscmnd  19444  ring1ne0  19875  unitmulclb  19952  isdrngd  20061  issrngd  20166  rmodislmodlem  20235  rmodislmod  20236  rmodislmodOLD  20237  abvn0b  20618  isphld  20904  mpfaddcl  21360  mpfmulcl  21361  pf1addcl  21564  pf1mulcl  21565  fitop  22094  hausnei2  22549  ordtt1  22575  locfincmp  22722  basqtop  22907  filfi  23055  fgcl  23074  neifil  23076  filuni  23081  cnextcn  23263  prdsmet  23568  blssps  23622  blss  23623  metcnp3  23741  hlhil  24652  volsup2  24814  sincosq1sgn  25700  sincosq2sgn  25701  sincosq3sgn  25702  sincosq4sgn  25703  sinq12ge0  25710  bcmono  26470  iswlkg  28025  umgrwwlks2on  28367  clwlkclwwlkfo  28418  3cyclfrgrrn1  28694  grpodivf  28945  ipf  29120  shintcli  29736  spanuni  29951  adjadj  30343  unopadj2  30345  hmopadj  30346  hmopbdoptHIL  30395  resvsca  31574  resvlem  31575  resvlemOLD  31576  submateq  31804  esumcocn  32093  bnj1379  32855  bnj571  32931  bnj594  32937  bnj580  32938  bnj600  32944  bnj1189  33034  bnj1321  33052  bnj1384  33057  f1resrcmplf1dlem  33103  hashfundm  33119  cplgredgex  33127  cusgr3cyclex  33143  loop1cycl  33144  umgr2cycllem  33147  umgr2cycl  33148  acycgr2v  33157  cusgracyclt3v  33163  climuzcnv  33674  fness  34583  bj-idreseq  35377  bj-imdiridlem  35400  neificl  35955  metf1o  35957  isismty  36003  ismtybndlem  36008  ablo4pnp  36082  divrngcl  36159  keridl  36234  prnc  36269  lsmsatcv  37066  llncvrlpln2  37613  lplncvrlvol2  37671  linepsubN  37808  pmapsub  37824  dalawlem10  37936  dalawlem13  37939  dalawlem14  37940  dalaw  37942  diaf11N  39105  dibf11N  39217  ismrcd1  40557  ismrcd2  40558  mzpincl  40593  mzpadd  40597  mzpmul  40598  pellfundge  40741  imasgim  40963  sqrtcval  41287  stoweidlem2  43592  stoweidlem17  43607  imaelsetpreimafv  44905  opnneir  46258  i0oii  46271  io1ii  46272