Theorem impr 458

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  reximddv2  3237  moi2  3655  preq12bg  4744  disjxiun  5027  disjxun  5028  wereu2  5516  f1ocnv2d  7378  funeldmdif  7729  extmptsuppeq  7837  suppssr  7844  omeulem1  8191  oelim2  8204  oeoa  8206  boxriin  8487  frfi  8747  fipreima  8814  marypha1lem  8881  supiso  8923  ordtypelem10  8975  r1ordg  9191  infxpenc2lem1  9430  acndom  9462  acndom2  9465  cofsmo  9680  cfcoflem  9683  fin23lem28  9751  fin23lem36  9759  isf32lem1  9764  isf32lem2  9765  isf32lem5  9768  isf34lem4  9788  fin1a2lem6  9816  fin1a2s  9825  ttukeylem2  9921  ttukeylem6  9925  fpwwe2lem8  10048  fpwwe2lem12  10052  inar1  10186  grudomon  10228  axpre-sup  10580  un0addcl  11918  un0mulcl  11919  peano2uz2  12058  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  xlemul1a  12669  fzadd2  12937  elfz2nn0  12993  fzind2  13150  expaddz  13469  expmulz  13471  swrdswrd  14058  cau3lem  14706  lo1bdd2  14873  climuni  14901  fsumcom2  15121  fprodcom2  15330  dvdsval2  15602  algcvga  15913  lcmgcdlem  15940  coprmproddvdslem  15996  divgcdcoprmex  16000  iserodd  16162  prmpwdvds  16230  ram0  16348  catpropd  16971  mndind  17984  isgrpinv  18148  gicsubgen  18410  sylow2alem2  18735  sylow2a  18736  frgpuptinv  18889  gsumcom3fi  19092  gsumxp2  19093  ablfac1eu  19188  dvdsrcl2  19396  islss4  19727  lspsnel6  19759  lmhmima  19812  lsmcl  19848  psgnodpm  20277  dsmmlss  20433  islindf4  20527  gsumbagdiag  20614  psrass1lem  20615  coe1tmmul2  20905  dmatscmcl  21108  mdetdiaglem  21203  mdetunilem9  21225  pm2mp  21430  epttop  21614  neindisj  21722  neitr  21785  restcls  21786  restntr  21787  ordtrest2lem  21808  cncnp  21885  cnconst  21889  1stcrest  22058  2ndcdisj  22061  2ndcsep  22064  1stccnp  22067  islly2  22089  1stckgenlem  22158  ptbasin  22182  ptbasfi  22186  ptcnplem  22226  ptcnp  22227  tx1stc  22255  qtophmeo  22422  filconn  22488  filuni  22490  ufileu  22524  elfm3  22555  rnelfmlem  22557  fmfnfmlem4  22562  cnpflf2  22605  alexsubALTlem4  22655  ptcmplem3  22659  ptcmplem4  22660  ptcmplem5  22661  tsmsxplem1  22758  bl2in  23007  metcnpi  23151  metcnpi2  23152  metcnpi3  23153  recld2  23419  icoopnst  23544  iocopnst  23545  ncvs1  23762  iscfil3  23877  iscmet3lem2  23896  ovoliunlem1  24106  ovolicc2lem2  24122  ovolicc2lem4  24124  voliun  24158  volsuplem  24159  dyadmbllem  24203  mbfinf  24269  mbflimsup  24270  itg2seq  24346  itg2splitlem  24352  itg2cnlem1  24365  ellimc3  24482  dvnadd  24532  dvcnvlem  24579  c1liplem1  24599  lhop2  24618  coe1mul3  24700  ply1divex  24737  dvdsq1p  24761  aannenlem1  24924  aalioulem2  24929  dvtaylp  24965  ulmdvlem3  24997  iblulm  25002  cxpmul2z  25282  xrlimcnp  25554  lgambdd  25622  wilthlem2  25654  basellem3  25668  dvdsflsumcom  25773  perfect  25815  dchreq  25842  dchrsum  25853  bposlem1  25868  lgsquad2  25970  dchrisum0fno1  26095  pntibnd  26177  oppperpex  26547  lmieu  26578  ax5seglem5  26727  axeuclid  26757  egrsubgr  27067  nbumgrvtx  27136  wwlksnextsurj  27686  clwwlkccat  27775  numclwwlk2lem1lem  28127  nmcvcn  28478  ubthlem1  28653  leopmul2i  29918  hstel2  30002  atom1d  30136  cdj1i  30216  f1o3d  30386  fsuppcurry1  30487  fsuppcurry2  30488  xrge0addge  30507  prmidl0  31034  mxidlmax  31045  reff  31192  ordtrest2NEWlem  31275  esumcst  31432  eulerpartlemgh  31746  cvmscld  32633  frpomin  33191  cgrxfr  33629  finminlem  33779  nn0prpwlem  33783  neibastop1  33820  neibastop2lem  33821  tailfb  33838  fvineqsneu  34828  pibt2  34834  finixpnum  35042  lindsenlbs  35052  matunitlindflem2  35054  poimirlem4  35061  poimirlem25  35082  poimirlem26  35083  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  heicant  35092  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  itg2addnclem3  35110  ftc1anc  35138  subspopn  35190  prdsbnd  35231  heibor1lem  35247  heiborlem1  35249  heibor  35259  isdrngo2  35396  rngoisocnv  35419  maxidlmax  35481  riotasv3d  36256  lkrpssN  36459  intnatN  36703  elpaddatiN  37101  pexmidlem5N  37270  lhpj1  37318  ltrnu  37417  cdlemn11pre  38506  dihord2pre  38521  dih1dimatlem0  38624  lcfrlem9  38846  remulcand  39575  0prjspnrel  39613  rexrabdioph  39735  ctbnfien  39759  irrapxlem3  39765  elpell14qr2  39803  elpell1qr2  39813  kelac1  40007  iunrelexpuztr  40420  rfovcnvfvd  40708  radcnvrat  41018  nznngen  41020  tz6.12-afv  43729  tz6.12-afv2  43796  iccelpart  43950  prproropf1olem3  44022  lighneallem4  44128  perfectALTV  44241  bgoldbtbndlem3  44325  tgoldbach  44335  isomuspgr  44352  isassintop  44470  ellcoellss  44844  lindslinindsimp2  44872  itscnhlinecirc02plem3  45198  inlinecirc02p  45201  aacllem  45329