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  3197  vtoclgft  3498  moi2  3663  preq12bg  4797  disjxiun  5083  disjxun  5084  wereu2  5619  frpomin  6296  f1ocnv2d  7611  funeldmdif  7992  extmptsuppeq  8129  suppssr  8136  suppssrg  8137  omeulem1  8508  oelim2  8522  oeoa  8524  boxriin  8879  frfi  9186  fipreima  9259  marypha1lem  9337  supiso  9380  ordtypelem10  9433  r1ordg  9691  infxpenc2lem1  9930  acndom  9962  acndom2  9965  cofsmo  10180  cfcoflem  10183  fin23lem28  10251  fin23lem36  10259  isf32lem1  10264  isf32lem2  10265  isf32lem5  10268  isf34lem4  10288  fin1a2lem6  10316  fin1a2s  10325  ttukeylem2  10421  ttukeylem6  10425  fpwwe2lem7  10549  fpwwe2lem11  10553  inar1  10687  grudomon  10729  axpre-sup  11081  un0addcl  12435  un0mulcl  12436  peano2uz2  12581  rpnnen1lem2  12891  rpnnen1lem1  12892  rpnnen1lem3  12893  rpnnen1lem5  12895  xlemul1a  13204  fzadd2  13476  elfz2nn0  13535  fzind2  13705  expaddz  14030  expmulz  14032  swrdswrd  14629  cau3lem  15279  lo1bdd2  15448  climuni  15476  fsumcom2  15698  fprodcom2  15908  dvdsval2  16183  algcvga  16507  lcmgcdlem  16534  coprmproddvdslem  16590  divgcdcoprmex  16594  iserodd  16764  prmpwdvds  16833  ram0  16951  catpropd  17633  mndind  18754  isgrpinv  18927  gicsubgen  19212  sylow2alem2  19551  sylow2a  19552  frgpuptinv  19704  gsumcom3fi  19912  gsumxp2  19913  ablfac1eu  20008  dvdsrcl2  20304  islss4  20915  ellspsn6  20947  lmhmima  21001  lsmcl  21037  psgnodpm  21545  dsmmlss  21701  islindf4  21795  gsumbagdiag  21888  psrass1lem  21889  coe1tmmul2  22219  dmatscmcl  22446  mdetdiaglem  22541  mdetunilem9  22563  pm2mp  22768  epttop  22952  neindisj  23060  neitr  23123  restcls  23124  restntr  23125  ordtrest2lem  23146  cncnp  23223  cnconst  23227  1stcrest  23396  2ndcdisj  23399  2ndcsep  23402  1stccnp  23405  islly2  23427  1stckgenlem  23496  ptbasin  23520  ptbasfi  23524  ptcnplem  23564  ptcnp  23565  tx1stc  23593  qtophmeo  23760  filconn  23826  filuni  23828  ufileu  23862  elfm3  23893  rnelfmlem  23895  fmfnfmlem4  23900  cnpflf2  23943  alexsubALTlem4  23993  ptcmplem3  23997  ptcmplem4  23998  ptcmplem5  23999  tsmsxplem1  24096  bl2in  24343  metcnpi  24487  metcnpi2  24488  metcnpi3  24489  recld2  24758  icoopnst  24884  iocopnst  24885  ncvs1  25102  iscfil3  25218  iscmet3lem2  25237  ovoliunlem1  25447  ovolicc2lem2  25463  ovolicc2lem4  25465  voliun  25499  volsuplem  25500  dyadmbllem  25544  mbfinf  25610  mbflimsup  25611  itg2seq  25687  itg2splitlem  25693  itg2cnlem1  25706  ellimc3  25824  dvnadd  25874  dvcnvlem  25921  c1liplem1  25942  lhop2  25961  coe1mul3  26045  ply1divex  26083  dvdsq1p  26109  aannenlem1  26276  aalioulem2  26281  dvtaylp  26318  ulmdvlem3  26351  iblulm  26356  cxpmul2z  26640  xrlimcnp  26918  lgambdd  26987  wilthlem2  27019  basellem3  27033  dvdsflsumcom  27138  perfect  27182  dchreq  27209  dchrsum  27220  bposlem1  27235  lgsquad2  27337  dchrisum0fno1  27462  pntibnd  27544  noinfbnd1lem4  27678  cuteq1  27797  madebdaylemlrcut  27879  precsexlem11  28197  recsex  28199  bdayons  28256  addonbday  28259  noseqp1  28271  noseqrdgfn  28286  bdaypw2n0bndlem  28443  bdayfinbndlem1  28447  remulscllem2  28481  oppperpex  28809  lmieu  28840  ax5seglem5  28990  axeuclid  29020  egrsubgr  29334  nbumgrvtx  29403  wwlksnextsurj  29957  clwwlkccat  30049  numclwwlk2lem1lem  30401  nmcvcn  30755  ubthlem1  30930  leopmul2i  32195  hstel2  32279  atom1d  32413  cdj1i  32493  f1o3d  32688  fsuppcurry1  32786  fsuppcurry2  32787  xrge0addge  32821  isdrng4  33361  prmidl0  33515  mxidlmax  33530  reff  33989  ordtrest2NEWlem  34072  esumcst  34213  eulerpartlemgh  34528  cvmscld  35461  cgrxfr  36243  finminlem  36506  nn0prpwlem  36510  neibastop1  36547  neibastop2lem  36548  tailfb  36565  fvineqsneu  37723  pibt2  37729  finixpnum  37917  lindsenlbs  37927  matunitlindflem2  37929  poimirlem4  37936  poimirlem25  37957  poimirlem26  37958  poimirlem29  37961  poimirlem30  37962  poimirlem31  37963  poimirlem32  37964  heicant  37967  mblfinlem3  37971  mblfinlem4  37972  itg2addnclem  37983  itg2addnclem3  37985  ftc1anc  38013  subspopn  38064  prdsbnd  38105  heibor1lem  38121  heiborlem1  38123  heibor  38133  isdrngo2  38270  rngoisocnv  38293  maxidlmax  38355  riotasv3d  39397  lkrpssN  39600  intnatN  39844  elpaddatiN  40242  pexmidlem5N  40411  lhpj1  40459  ltrnu  40558  cdlemn11pre  41647  dihord2pre  41662  dih1dimatlem0  41765  lcfrlem9  41987  remulcand  42870  prjspner1  43058  0prjspnrel  43059  nna4b4nsq  43092  rexrabdioph  43225  ctbnfien  43249  irrapxlem3  43255  elpell14qr2  43293  elpell1qr2  43303  kelac1  43494  iunrelexpuztr  44149  rfovcnvfvd  44437  radcnvrat  44744  nznngen  44746  tz6.12-afv  47607  tz6.12-afv2  47674  iccelpart  47867  prproropf1olem3  47939  lighneallem4  48044  perfectALTV  48157  bgoldbtbndlem3  48241  tgoldbach  48251  grimcnv  48322  grimco  48323  isuspgrim0  48328  grimedg  48369  isubgr3stgrlem7  48406  gpg5nbgrvtx03starlem1  48502  gpg5nbgrvtx03starlem3  48504  gpg5nbgrvtx13starlem1  48505  gpg5nbgrvtx13starlem3  48507  isassintop  48644  ellcoellss  48869  lindslinindsimp2  48897  itscnhlinecirc02plem3  49218  inlinecirc02p  49221  aacllem  50234