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  3194  vtoclgft  3495  moi2  3659  preq12bg  4786  disjxiun  5071  disjxun  5072  wereu2  5617  frpomin  6293  f1ocnv2d  7609  funeldmdif  7990  extmptsuppeq  8127  suppssr  8134  suppssrg  8135  omeulem1  8506  oelim2  8520  oeoa  8522  boxriin  8877  frfi  9184  fipreima  9257  marypha1lem  9335  supiso  9378  ordtypelem10  9431  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  12459  un0mulcl  12460  peano2uz2  12606  rpnnen1lem2  12916  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem5  12920  xlemul1a  13229  fzadd2  13502  elfz2nn0  13561  fzind2  13732  expaddz  14057  expmulz  14059  swrdswrd  14656  cau3lem  15306  lo1bdd2  15475  climuni  15503  fsumcom2  15725  fprodcom2  15938  dvdsval2  16213  algcvga  16537  lcmgcdlem  16564  coprmproddvdslem  16620  divgcdcoprmex  16624  iserodd  16795  prmpwdvds  16864  ram0  16982  catpropd  17664  mndind  18785  isgrpinv  18958  gicsubgen  19243  sylow2alem2  19582  sylow2a  19583  frgpuptinv  19735  gsumcom3fi  19943  gsumxp2  19944  ablfac1eu  20039  dvdsrcl2  20335  islss4  20946  ellspsn6  20978  lmhmima  21031  lsmcl  21067  psgnodpm  21557  dsmmlss  21713  islindf4  21807  gsumbagdiag  21900  psrass1lem  21901  coe1tmmul2  22229  dmatscmcl  22456  mdetdiaglem  22551  mdetunilem9  22573  pm2mp  22778  epttop  22962  neindisj  23070  neitr  23133  restcls  23134  restntr  23135  ordtrest2lem  23156  cncnp  23233  cnconst  23237  1stcrest  23406  2ndcdisj  23409  2ndcsep  23412  1stccnp  23415  islly2  23437  1stckgenlem  23506  ptbasin  23530  ptbasfi  23534  ptcnplem  23574  ptcnp  23575  tx1stc  23603  qtophmeo  23770  filconn  23836  filuni  23838  ufileu  23872  elfm3  23903  rnelfmlem  23905  fmfnfmlem4  23910  cnpflf2  23953  alexsubALTlem4  24003  ptcmplem3  24007  ptcmplem4  24008  ptcmplem5  24009  tsmsxplem1  24106  bl2in  24353  metcnpi  24497  metcnpi2  24498  metcnpi3  24499  recld2  24768  icoopnst  24894  iocopnst  24895  ncvs1  25112  iscfil3  25228  iscmet3lem2  25247  ovoliunlem1  25457  ovolicc2lem2  25473  ovolicc2lem4  25475  voliun  25509  volsuplem  25510  dyadmbllem  25554  mbfinf  25620  mbflimsup  25621  itg2seq  25697  itg2splitlem  25703  itg2cnlem1  25716  ellimc3  25834  dvnadd  25884  dvcnvlem  25931  c1liplem1  25951  lhop2  25970  coe1mul3  26052  ply1divex  26090  dvdsq1p  26116  aannenlem1  26282  aalioulem2  26287  dvtaylp  26323  ulmdvlem3  26355  iblulm  26360  cxpmul2z  26643  xrlimcnp  26920  lgambdd  26988  wilthlem2  27020  basellem3  27034  dvdsflsumcom  27139  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  29956  clwwlkccat  30048  numclwwlk2lem1lem  30400  nmcvcn  30754  ubthlem1  30929  leopmul2i  32194  hstel2  32278  atom1d  32412  cdj1i  32492  f1o3d  32687  fsuppcurry1  32785  fsuppcurry2  32786  xrge0addge  32819  isdrng4  33344  prmidl0  33498  mxidlmax  33513  reff  33971  ordtrest2NEWlem  34054  esumcst  34195  eulerpartlemgh  34510  cvmscld  35443  cgrxfr  36225  finminlem  36488  nn0prpwlem  36492  neibastop1  36529  neibastop2lem  36530  tailfb  36547  fvineqsneu  37715  pibt2  37721  finixpnum  37914  lindsenlbs  37924  matunitlindflem2  37926  poimirlem4  37933  poimirlem25  37954  poimirlem26  37955  poimirlem29  37958  poimirlem30  37959  poimirlem31  37960  poimirlem32  37961  heicant  37964  mblfinlem3  37968  mblfinlem4  37969  itg2addnclem  37980  itg2addnclem3  37982  ftc1anc  38010  subspopn  38061  prdsbnd  38102  heibor1lem  38118  heiborlem1  38120  heibor  38130  isdrngo2  38267  rngoisocnv  38290  maxidlmax  38352  riotasv3d  39394  lkrpssN  39597  intnatN  39841  elpaddatiN  40239  pexmidlem5N  40408  lhpj1  40456  ltrnu  40555  cdlemn11pre  41644  dihord2pre  41659  dih1dimatlem0  41762  lcfrlem9  41984  remulcand  42859  prjspner1  43047  0prjspnrel  43048  nna4b4nsq  43081  rexrabdioph  43210  ctbnfien  43234  irrapxlem3  43240  elpell14qr2  43278  elpell1qr2  43288  kelac1  43479  iunrelexpuztr  44134  rfovcnvfvd  44422  radcnvrat  44729  nznngen  44731  tz6.12-afv  47609  tz6.12-afv2  47676  iccelpart  47881  prproropf1olem3  47953  lighneallem4  48061  perfectALTV  48187  bgoldbtbndlem3  48271  tgoldbach  48281  grimcnv  48352  grimco  48353  isuspgrim0  48358  grimedg  48399  isubgr3stgrlem7  48436  gpg5nbgrvtx03starlem1  48532  gpg5nbgrvtx03starlem3  48534  gpg5nbgrvtx13starlem1  48535  gpg5nbgrvtx13starlem3  48537  isassintop  48674  ellcoellss  48899  lindslinindsimp2  48927  itscnhlinecirc02plem3  49248  inlinecirc02p  49251  aacllem  50264