Theorem 3expib 1260

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anidm12  1375  mob  3355  eqbrrdva  5213  fco  5971  f1oiso2  6502  frxp  7174  onfununi  7325  smoel2  7347  smoiso2  7353  3ecoptocl  7726  dffi2  8212  elfiun  8219  dif1card  8716  infxpenlem  8719  cfeq0  8961  cfsuc  8962  cfflb  8964  cfslb2n  8973  cofsmo  8974  domtriomlem  9147  axdc3lem4  9158  axdc4lem  9160  ttukey2g  9221  tskxpss  9473  grudomon  9518  elnpi  9689  dedekind  10079  nn0n0n1ge2b  11236  fzind  11351  suprzcl2  11654  icoshft  12165  fzen  12229  hashbclem  13093  seqcoll  13105  relexpsucr  13617  relexpsucl  13621  relexpfld  13637  shftuz  13657  mulgcd  15103  algcvga  15130  lcmneg  15154  ressbas  15757  resslem  15760  ressress  15765  psss  17037  tsrlemax  17043  isnmgm  17069  gsummgmpropd  17098  iscmnd  18028  ring1ne0  18414  unitmulclb  18488  isdrngd  18595  issrngd  18684  abvn0b  19123  mpfaddcl  19355  mpfmulcl  19356  pf1addcl  19538  pf1mulcl  19539  isphld  19818  fitop  20530  hausnei2  20967  ordtt1  20993  locfincmp  21139  basqtop  21324  filfi  21473  fgcl  21492  neifil  21494  filuni  21499  cnextcn  21681  prdsmet  21985  blssps  22039  blss  22040  metcnp3  22155  hlhil  23022  volsup2  23179  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  sinq12ge0  24064  bcmono  24802  usg2wlkonot  26410  3cyclfrgrarn1  26539  grpodivf  26776  ipf  26952  shintcli  27572  spanuni  27787  adjadj  28179  unopadj2  28181  hmopadj  28182  hmopbdoptHIL  28231  resvsca  29161  resvlem  29162  submateq  29203  esumcocn  29469  bnj1379  30155  bnj571  30230  bnj594  30236  bnj580  30237  bnj600  30243  bnj1189  30331  bnj1321  30349  bnj1384  30354  climuzcnv  30819  fness  31514  neificl  32719  metf1o  32721  isismty  32770  ismtybndlem  32775  ablo4pnp  32849  divrngcl  32926  keridl  33001  prnc  33036  lsmsatcv  33315  llncvrlpln2  33861  lplncvrlvol2  33919  linepsubN  34056  pmapsub  34072  dalawlem10  34184  dalawlem13  34187  dalawlem14  34188  dalaw  34190  diaf11N  35356  dibf11N  35468  ismrcd1  36279  ismrcd2  36280  mzpincl  36315  mzpadd  36319  mzpmul  36320  pellfundge  36464  imasgim  36688  stoweidlem2  38895  stoweidlem17  38910  uhgrauhgrbi  40377  is1wlkg  40816  uspgrn2crct  41011  umgrwwlks2on  41161  3cyclfrgrrn1  41455