Theorem impr 455

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 413	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 419	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reximddv2  3202  moi2  3677  preq12bg  4816  disjxiun  5107  disjxun  5108  wereu2  5635  frpomin  6299  f1ocnv2d  7611  funeldmdif  7985  extmptsuppeq  8124  suppssr  8132  suppssrg  8133  omeulem1  8534  oelim2  8547  oeoa  8549  boxriin  8885  frfi  9239  fipreima  9309  marypha1lem  9378  supiso  9420  ordtypelem10  9472  r1ordg  9723  infxpenc2lem1  9964  acndom  9996  acndom2  9999  cofsmo  10214  cfcoflem  10217  fin23lem28  10285  fin23lem36  10293  isf32lem1  10298  isf32lem2  10299  isf32lem5  10302  isf34lem4  10322  fin1a2lem6  10350  fin1a2s  10359  ttukeylem2  10455  ttukeylem6  10459  fpwwe2lem7  10582  fpwwe2lem11  10586  inar1  10720  grudomon  10762  axpre-sup  11114  un0addcl  12455  un0mulcl  12456  peano2uz2  12600  rpnnen1lem2  12911  rpnnen1lem1  12912  rpnnen1lem3  12913  rpnnen1lem5  12915  xlemul1a  13217  fzadd2  13486  elfz2nn0  13542  fzind2  13700  expaddz  14022  expmulz  14024  swrdswrd  14605  cau3lem  15251  lo1bdd2  15418  climuni  15446  fsumcom2  15670  fprodcom2  15878  dvdsval2  16150  algcvga  16466  lcmgcdlem  16493  coprmproddvdslem  16549  divgcdcoprmex  16553  iserodd  16718  prmpwdvds  16787  ram0  16905  catpropd  17603  mndind  18652  isgrpinv  18818  gicsubgen  19082  sylow2alem2  19414  sylow2a  19415  frgpuptinv  19567  gsumcom3fi  19770  gsumxp2  19771  ablfac1eu  19866  dvdsrcl2  20093  islss4  20480  lspsnel6  20512  lmhmima  20565  lsmcl  20601  psgnodpm  21029  dsmmlss  21187  islindf4  21281  gsumbagdiagOLD  21378  psrass1lemOLD  21379  gsumbagdiag  21381  psrass1lem  21382  coe1tmmul2  21684  dmatscmcl  21889  mdetdiaglem  21984  mdetunilem9  22006  pm2mp  22211  epttop  22396  neindisj  22505  neitr  22568  restcls  22569  restntr  22570  ordtrest2lem  22591  cncnp  22668  cnconst  22672  1stcrest  22841  2ndcdisj  22844  2ndcsep  22847  1stccnp  22850  islly2  22872  1stckgenlem  22941  ptbasin  22965  ptbasfi  22969  ptcnplem  23009  ptcnp  23010  tx1stc  23038  qtophmeo  23205  filconn  23271  filuni  23273  ufileu  23307  elfm3  23338  rnelfmlem  23340  fmfnfmlem4  23345  cnpflf2  23388  alexsubALTlem4  23438  ptcmplem3  23442  ptcmplem4  23443  ptcmplem5  23444  tsmsxplem1  23541  bl2in  23790  metcnpi  23937  metcnpi2  23938  metcnpi3  23939  recld2  24214  icoopnst  24339  iocopnst  24340  ncvs1  24558  iscfil3  24674  iscmet3lem2  24693  ovoliunlem1  24903  ovolicc2lem2  24919  ovolicc2lem4  24921  voliun  24955  volsuplem  24956  dyadmbllem  25000  mbfinf  25066  mbflimsup  25067  itg2seq  25144  itg2splitlem  25150  itg2cnlem1  25163  ellimc3  25280  dvnadd  25330  dvcnvlem  25377  c1liplem1  25397  lhop2  25416  coe1mul3  25501  ply1divex  25538  dvdsq1p  25562  aannenlem1  25725  aalioulem2  25730  dvtaylp  25766  ulmdvlem3  25798  iblulm  25803  cxpmul2z  26083  xrlimcnp  26355  lgambdd  26423  wilthlem2  26455  basellem3  26469  dvdsflsumcom  26574  perfect  26616  dchreq  26643  dchrsum  26654  bposlem1  26669  lgsquad2  26771  dchrisum0fno1  26896  pntibnd  26978  noinfbnd1lem4  27111  madebdaylemlrcut  27271  oppperpex  27758  lmieu  27789  ax5seglem5  27945  axeuclid  27975  egrsubgr  28288  nbumgrvtx  28357  wwlksnextsurj  28908  clwwlkccat  28997  numclwwlk2lem1lem  29349  nmcvcn  29700  ubthlem1  29875  leopmul2i  31140  hstel2  31224  atom1d  31358  cdj1i  31438  f1o3d  31608  fsuppcurry1  31710  fsuppcurry2  31711  xrge0addge  31730  prmidl0  32299  mxidlmax  32310  reff  32509  ordtrest2NEWlem  32592  esumcst  32751  eulerpartlemgh  33067  cvmscld  33954  cgrxfr  34716  finminlem  34866  nn0prpwlem  34870  neibastop1  34907  neibastop2lem  34908  tailfb  34925  fvineqsneu  35955  pibt2  35961  finixpnum  36136  lindsenlbs  36146  matunitlindflem2  36148  poimirlem4  36155  poimirlem25  36176  poimirlem26  36177  poimirlem29  36180  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  heicant  36186  mblfinlem3  36190  mblfinlem4  36191  itg2addnclem  36202  itg2addnclem3  36204  ftc1anc  36232  subspopn  36284  prdsbnd  36325  heibor1lem  36341  heiborlem1  36343  heibor  36353  isdrngo2  36490  rngoisocnv  36513  maxidlmax  36575  riotasv3d  37495  lkrpssN  37698  intnatN  37943  elpaddatiN  38341  pexmidlem5N  38510  lhpj1  38558  ltrnu  38657  cdlemn11pre  39746  dihord2pre  39761  dih1dimatlem0  39864  lcfrlem9  40086  remulcand  40965  prjspner1  41022  0prjspnrel  41023  nna4b4nsq  41056  rexrabdioph  41175  ctbnfien  41199  irrapxlem3  41205  elpell14qr2  41243  elpell1qr2  41253  kelac1  41448  iunrelexpuztr  42113  rfovcnvfvd  42401  radcnvrat  42716  nznngen  42718  tz6.12-afv  45525  tz6.12-afv2  45592  iccelpart  45745  prproropf1olem3  45817  lighneallem4  45922  perfectALTV  46035  bgoldbtbndlem3  46119  tgoldbach  46129  isomuspgr  46146  isassintop  46264  ellcoellss  46636  lindslinindsimp2  46664  itscnhlinecirc02plem3  46990  inlinecirc02p  46993  aacllem  47368