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  3191  vtoclgft  3505  moi2  3670  preq12bg  4802  disjxiun  5086  disjxun  5087  wereu2  5611  frpomin  6287  f1ocnv2d  7599  funeldmdif  7980  extmptsuppeq  8118  suppssr  8125  suppssrg  8126  omeulem1  8497  oelim2  8510  oeoa  8512  boxriin  8864  frfi  9169  fipreima  9242  marypha1lem  9317  supiso  9360  ordtypelem10  9413  r1ordg  9671  infxpenc2lem1  9910  acndom  9942  acndom2  9945  cofsmo  10160  cfcoflem  10163  fin23lem28  10231  fin23lem36  10239  isf32lem1  10244  isf32lem2  10245  isf32lem5  10248  isf34lem4  10268  fin1a2lem6  10296  fin1a2s  10305  ttukeylem2  10401  ttukeylem6  10405  fpwwe2lem7  10528  fpwwe2lem11  10532  inar1  10666  grudomon  10708  axpre-sup  11060  un0addcl  12414  un0mulcl  12415  peano2uz2  12561  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  xlemul1a  13187  fzadd2  13459  elfz2nn0  13518  fzind2  13688  expaddz  14013  expmulz  14015  swrdswrd  14612  cau3lem  15262  lo1bdd2  15431  climuni  15459  fsumcom2  15681  fprodcom2  15891  dvdsval2  16166  algcvga  16490  lcmgcdlem  16517  coprmproddvdslem  16573  divgcdcoprmex  16577  iserodd  16747  prmpwdvds  16816  ram0  16934  catpropd  17615  mndind  18736  isgrpinv  18906  gicsubgen  19191  sylow2alem2  19530  sylow2a  19531  frgpuptinv  19683  gsumcom3fi  19891  gsumxp2  19892  ablfac1eu  19987  dvdsrcl2  20284  islss4  20895  ellspsn6  20927  lmhmima  20981  lsmcl  21017  psgnodpm  21525  dsmmlss  21681  islindf4  21775  gsumbagdiag  21868  psrass1lem  21869  coe1tmmul2  22190  dmatscmcl  22418  mdetdiaglem  22513  mdetunilem9  22535  pm2mp  22740  epttop  22924  neindisj  23032  neitr  23095  restcls  23096  restntr  23097  ordtrest2lem  23118  cncnp  23195  cnconst  23199  1stcrest  23368  2ndcdisj  23371  2ndcsep  23374  1stccnp  23377  islly2  23399  1stckgenlem  23468  ptbasin  23492  ptbasfi  23496  ptcnplem  23536  ptcnp  23537  tx1stc  23565  qtophmeo  23732  filconn  23798  filuni  23800  ufileu  23834  elfm3  23865  rnelfmlem  23867  fmfnfmlem4  23872  cnpflf2  23915  alexsubALTlem4  23965  ptcmplem3  23969  ptcmplem4  23970  ptcmplem5  23971  tsmsxplem1  24068  bl2in  24315  metcnpi  24459  metcnpi2  24460  metcnpi3  24461  recld2  24730  icoopnst  24863  iocopnst  24864  ncvs1  25084  iscfil3  25200  iscmet3lem2  25219  ovoliunlem1  25430  ovolicc2lem2  25446  ovolicc2lem4  25448  voliun  25482  volsuplem  25483  dyadmbllem  25527  mbfinf  25593  mbflimsup  25594  itg2seq  25670  itg2splitlem  25676  itg2cnlem1  25689  ellimc3  25807  dvnadd  25858  dvcnvlem  25907  c1liplem1  25928  lhop2  25947  coe1mul3  26031  ply1divex  26069  dvdsq1p  26095  aannenlem1  26263  aalioulem2  26268  dvtaylp  26305  ulmdvlem3  26338  iblulm  26343  cxpmul2z  26627  xrlimcnp  26905  lgambdd  26974  wilthlem2  27006  basellem3  27020  dvdsflsumcom  27125  perfect  27169  dchreq  27196  dchrsum  27207  bposlem1  27222  lgsquad2  27324  dchrisum0fno1  27449  pntibnd  27531  noinfbnd1lem4  27665  cuteq1  27778  madebdaylemlrcut  27844  precsexlem11  28155  recsex  28157  bdayon  28209  noseqp1  28221  noseqrdgfn  28236  remulscllem2  28403  oppperpex  28731  lmieu  28762  ax5seglem5  28911  axeuclid  28941  egrsubgr  29255  nbumgrvtx  29324  wwlksnextsurj  29878  clwwlkccat  29970  numclwwlk2lem1lem  30322  nmcvcn  30675  ubthlem1  30850  leopmul2i  32115  hstel2  32199  atom1d  32333  cdj1i  32413  f1o3d  32608  fsuppcurry1  32707  fsuppcurry2  32708  xrge0addge  32741  isdrng4  33261  prmidl0  33415  mxidlmax  33430  reff  33852  ordtrest2NEWlem  33935  esumcst  34076  eulerpartlemgh  34391  cvmscld  35317  cgrxfr  36099  finminlem  36362  nn0prpwlem  36366  neibastop1  36403  neibastop2lem  36404  tailfb  36421  fvineqsneu  37455  pibt2  37461  finixpnum  37644  lindsenlbs  37654  matunitlindflem2  37656  poimirlem4  37663  poimirlem25  37684  poimirlem26  37685  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  heicant  37694  mblfinlem3  37698  mblfinlem4  37699  itg2addnclem  37710  itg2addnclem3  37712  ftc1anc  37740  subspopn  37791  prdsbnd  37832  heibor1lem  37848  heiborlem1  37850  heibor  37860  isdrngo2  37997  rngoisocnv  38020  maxidlmax  38082  riotasv3d  39058  lkrpssN  39261  intnatN  39505  elpaddatiN  39903  pexmidlem5N  40072  lhpj1  40120  ltrnu  40219  cdlemn11pre  41308  dihord2pre  41323  dih1dimatlem0  41426  lcfrlem9  41648  remulcand  42531  prjspner1  42718  0prjspnrel  42719  nna4b4nsq  42752  rexrabdioph  42886  ctbnfien  42910  irrapxlem3  42916  elpell14qr2  42954  elpell1qr2  42964  kelac1  43155  iunrelexpuztr  43811  rfovcnvfvd  44099  radcnvrat  44406  nznngen  44408  tz6.12-afv  47272  tz6.12-afv2  47339  iccelpart  47532  prproropf1olem3  47604  lighneallem4  47709  perfectALTV  47822  bgoldbtbndlem3  47906  tgoldbach  47916  grimcnv  47987  grimco  47988  isuspgrim0  47993  grimedg  48034  isubgr3stgrlem7  48071  gpg5nbgrvtx03starlem1  48167  gpg5nbgrvtx03starlem3  48169  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem3  48172  isassintop  48309  ellcoellss  48535  lindslinindsimp2  48563  itscnhlinecirc02plem3  48884  inlinecirc02p  48887  aacllem  49901