Theorem impr 454

Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
impr.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem impr

Step	Hyp	Ref	Expression
1		impr.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reximddv2  3215  vtoclgft  3552  moi2  3722  preq12bg  4853  disjxiun  5140  disjxun  5141  wereu2  5682  frpomin  6361  f1ocnv2d  7686  funeldmdif  8073  extmptsuppeq  8213  suppssr  8220  suppssrg  8221  omeulem1  8620  oelim2  8633  oeoa  8635  boxriin  8980  frfi  9321  fipreima  9398  marypha1lem  9473  supiso  9515  ordtypelem10  9567  r1ordg  9818  infxpenc2lem1  10059  acndom  10091  acndom2  10094  cofsmo  10309  cfcoflem  10312  fin23lem28  10380  fin23lem36  10388  isf32lem1  10393  isf32lem2  10394  isf32lem5  10397  isf34lem4  10417  fin1a2lem6  10445  fin1a2s  10454  ttukeylem2  10550  ttukeylem6  10554  fpwwe2lem7  10677  fpwwe2lem11  10681  inar1  10815  grudomon  10857  axpre-sup  11209  un0addcl  12559  un0mulcl  12560  peano2uz2  12706  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  xlemul1a  13330  fzadd2  13599  elfz2nn0  13658  fzind2  13824  expaddz  14147  expmulz  14149  swrdswrd  14743  cau3lem  15393  lo1bdd2  15560  climuni  15588  fsumcom2  15810  fprodcom2  16020  dvdsval2  16293  algcvga  16616  lcmgcdlem  16643  coprmproddvdslem  16699  divgcdcoprmex  16703  iserodd  16873  prmpwdvds  16942  ram0  17060  catpropd  17752  mndind  18841  isgrpinv  19011  gicsubgen  19297  sylow2alem2  19636  sylow2a  19637  frgpuptinv  19789  gsumcom3fi  19997  gsumxp2  19998  ablfac1eu  20093  dvdsrcl2  20366  islss4  20960  ellspsn6  20992  lmhmima  21046  lsmcl  21082  psgnodpm  21606  dsmmlss  21764  islindf4  21858  gsumbagdiag  21951  psrass1lem  21952  coe1tmmul2  22279  dmatscmcl  22509  mdetdiaglem  22604  mdetunilem9  22626  pm2mp  22831  epttop  23016  neindisj  23125  neitr  23188  restcls  23189  restntr  23190  ordtrest2lem  23211  cncnp  23288  cnconst  23292  1stcrest  23461  2ndcdisj  23464  2ndcsep  23467  1stccnp  23470  islly2  23492  1stckgenlem  23561  ptbasin  23585  ptbasfi  23589  ptcnplem  23629  ptcnp  23630  tx1stc  23658  qtophmeo  23825  filconn  23891  filuni  23893  ufileu  23927  elfm3  23958  rnelfmlem  23960  fmfnfmlem4  23965  cnpflf2  24008  alexsubALTlem4  24058  ptcmplem3  24062  ptcmplem4  24063  ptcmplem5  24064  tsmsxplem1  24161  bl2in  24410  metcnpi  24557  metcnpi2  24558  metcnpi3  24559  recld2  24836  icoopnst  24969  iocopnst  24970  ncvs1  25191  iscfil3  25307  iscmet3lem2  25326  ovoliunlem1  25537  ovolicc2lem2  25553  ovolicc2lem4  25555  voliun  25589  volsuplem  25590  dyadmbllem  25634  mbfinf  25700  mbflimsup  25701  itg2seq  25777  itg2splitlem  25783  itg2cnlem1  25796  ellimc3  25914  dvnadd  25965  dvcnvlem  26014  c1liplem1  26035  lhop2  26054  coe1mul3  26138  ply1divex  26176  dvdsq1p  26202  aannenlem1  26370  aalioulem2  26375  dvtaylp  26412  ulmdvlem3  26445  iblulm  26450  cxpmul2z  26733  xrlimcnp  27011  lgambdd  27080  wilthlem2  27112  basellem3  27126  dvdsflsumcom  27231  perfect  27275  dchreq  27302  dchrsum  27313  bposlem1  27328  lgsquad2  27430  dchrisum0fno1  27555  pntibnd  27637  noinfbnd1lem4  27771  cuteq1  27878  madebdaylemlrcut  27937  precsexlem11  28241  recsex  28243  noseqp1  28297  noseqrdgfn  28312  remulscllem2  28433  oppperpex  28761  lmieu  28792  ax5seglem5  28948  axeuclid  28978  egrsubgr  29294  nbumgrvtx  29363  wwlksnextsurj  29920  clwwlkccat  30009  numclwwlk2lem1lem  30361  nmcvcn  30714  ubthlem1  30889  leopmul2i  32154  hstel2  32238  atom1d  32372  cdj1i  32452  f1o3d  32637  fsuppcurry1  32736  fsuppcurry2  32737  xrge0addge  32761  isdrng4  33298  prmidl0  33478  mxidlmax  33493  reff  33838  ordtrest2NEWlem  33921  esumcst  34064  eulerpartlemgh  34380  cvmscld  35278  cgrxfr  36056  finminlem  36319  nn0prpwlem  36323  neibastop1  36360  neibastop2lem  36361  tailfb  36378  fvineqsneu  37412  pibt2  37418  finixpnum  37612  lindsenlbs  37622  matunitlindflem2  37624  poimirlem4  37631  poimirlem25  37652  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2addnclem3  37680  ftc1anc  37708  subspopn  37759  prdsbnd  37800  heibor1lem  37816  heiborlem1  37818  heibor  37828  isdrngo2  37965  rngoisocnv  37988  maxidlmax  38050  riotasv3d  38961  lkrpssN  39164  intnatN  39409  elpaddatiN  39807  pexmidlem5N  39976  lhpj1  40024  ltrnu  40123  cdlemn11pre  41212  dihord2pre  41227  dih1dimatlem0  41330  lcfrlem9  41552  remulcand  42468  prjspner1  42636  0prjspnrel  42637  nna4b4nsq  42670  rexrabdioph  42805  ctbnfien  42829  irrapxlem3  42835  elpell14qr2  42873  elpell1qr2  42883  kelac1  43075  iunrelexpuztr  43732  rfovcnvfvd  44020  radcnvrat  44333  nznngen  44335  tz6.12-afv  47185  tz6.12-afv2  47252  iccelpart  47420  prproropf1olem3  47492  lighneallem4  47597  perfectALTV  47710  bgoldbtbndlem3  47794  tgoldbach  47804  isuspgrim0  47872  uspgrimprop  47873  grimcnv  47879  grimco  47880  grimedg  47903  isubgr3stgrlem7  47939  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  isassintop  48126  ellcoellss  48352  lindslinindsimp2  48380  itscnhlinecirc02plem3  48705  inlinecirc02p  48708  aacllem  49320