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  3189  moi2  3616  preq12bg  4740  disjxiun  5028  disjxun  5029  wereu2  5523  f1ocnv2d  7417  funeldmdif  7775  extmptsuppeq  7886  suppssr  7894  suppssrg  7895  omeulem1  8242  oelim2  8255  oeoa  8257  boxriin  8553  frfi  8840  fipreima  8906  marypha1lem  8973  supiso  9015  ordtypelem10  9067  r1ordg  9283  infxpenc2lem1  9522  acndom  9554  acndom2  9557  cofsmo  9772  cfcoflem  9775  fin23lem28  9843  fin23lem36  9851  isf32lem1  9856  isf32lem2  9857  isf32lem5  9860  isf34lem4  9880  fin1a2lem6  9908  fin1a2s  9917  ttukeylem2  10013  ttukeylem6  10017  fpwwe2lem7  10140  fpwwe2lem11  10144  inar1  10278  grudomon  10320  axpre-sup  10672  un0addcl  12012  un0mulcl  12013  peano2uz2  12154  rpnnen1lem2  12462  rpnnen1lem1  12463  rpnnen1lem3  12464  rpnnen1lem5  12466  xlemul1a  12767  fzadd2  13036  elfz2nn0  13092  fzind2  13249  expaddz  13568  expmulz  13570  swrdswrd  14159  cau3lem  14807  lo1bdd2  14974  climuni  15002  fsumcom2  15225  fprodcom2  15433  dvdsval2  15705  algcvga  16023  lcmgcdlem  16050  coprmproddvdslem  16106  divgcdcoprmex  16110  iserodd  16275  prmpwdvds  16343  ram0  16461  catpropd  17086  mndind  18111  isgrpinv  18277  gicsubgen  18539  sylow2alem2  18864  sylow2a  18865  frgpuptinv  19018  gsumcom3fi  19221  gsumxp2  19222  ablfac1eu  19317  dvdsrcl2  19525  islss4  19856  lspsnel6  19888  lmhmima  19941  lsmcl  19977  psgnodpm  20407  dsmmlss  20563  islindf4  20657  gsumbagdiagOLD  20755  psrass1lemOLD  20756  gsumbagdiag  20758  psrass1lem  20759  coe1tmmul2  21054  dmatscmcl  21257  mdetdiaglem  21352  mdetunilem9  21374  pm2mp  21579  epttop  21763  neindisj  21871  neitr  21934  restcls  21935  restntr  21936  ordtrest2lem  21957  cncnp  22034  cnconst  22038  1stcrest  22207  2ndcdisj  22210  2ndcsep  22213  1stccnp  22216  islly2  22238  1stckgenlem  22307  ptbasin  22331  ptbasfi  22335  ptcnplem  22375  ptcnp  22376  tx1stc  22404  qtophmeo  22571  filconn  22637  filuni  22639  ufileu  22673  elfm3  22704  rnelfmlem  22706  fmfnfmlem4  22711  cnpflf2  22754  alexsubALTlem4  22804  ptcmplem3  22808  ptcmplem4  22809  ptcmplem5  22810  tsmsxplem1  22907  bl2in  23156  metcnpi  23300  metcnpi2  23301  metcnpi3  23302  recld2  23569  icoopnst  23694  iocopnst  23695  ncvs1  23912  iscfil3  24028  iscmet3lem2  24047  ovoliunlem1  24257  ovolicc2lem2  24273  ovolicc2lem4  24275  voliun  24309  volsuplem  24310  dyadmbllem  24354  mbfinf  24420  mbflimsup  24421  itg2seq  24498  itg2splitlem  24504  itg2cnlem1  24517  ellimc3  24634  dvnadd  24684  dvcnvlem  24731  c1liplem1  24751  lhop2  24770  coe1mul3  24855  ply1divex  24892  dvdsq1p  24916  aannenlem1  25079  aalioulem2  25084  dvtaylp  25120  ulmdvlem3  25152  iblulm  25157  cxpmul2z  25437  xrlimcnp  25709  lgambdd  25777  wilthlem2  25809  basellem3  25823  dvdsflsumcom  25928  perfect  25970  dchreq  25997  dchrsum  26008  bposlem1  26023  lgsquad2  26125  dchrisum0fno1  26250  pntibnd  26332  oppperpex  26702  lmieu  26733  ax5seglem5  26882  axeuclid  26912  egrsubgr  27222  nbumgrvtx  27291  wwlksnextsurj  27841  clwwlkccat  27930  numclwwlk2lem1lem  28282  nmcvcn  28633  ubthlem1  28808  leopmul2i  30073  hstel2  30157  atom1d  30291  cdj1i  30371  f1o3d  30539  fsuppcurry1  30638  fsuppcurry2  30639  xrge0addge  30658  prmidl0  31201  mxidlmax  31212  reff  31364  ordtrest2NEWlem  31447  esumcst  31604  eulerpartlemgh  31918  cvmscld  32809  frpomin  33386  noinfbnd1lem4  33575  madebdaylemlrcut  33725  cgrxfr  34003  finminlem  34153  nn0prpwlem  34157  neibastop1  34194  neibastop2lem  34195  tailfb  34212  fvineqsneu  35228  pibt2  35234  finixpnum  35408  lindsenlbs  35418  matunitlindflem2  35420  poimirlem4  35427  poimirlem25  35448  poimirlem26  35449  poimirlem29  35452  poimirlem30  35453  poimirlem31  35454  poimirlem32  35455  heicant  35458  mblfinlem3  35462  mblfinlem4  35463  itg2addnclem  35474  itg2addnclem3  35476  ftc1anc  35504  subspopn  35556  prdsbnd  35597  heibor1lem  35613  heiborlem1  35615  heibor  35625  isdrngo2  35762  rngoisocnv  35785  maxidlmax  35847  riotasv3d  36620  lkrpssN  36823  intnatN  37067  elpaddatiN  37465  pexmidlem5N  37634  lhpj1  37682  ltrnu  37781  cdlemn11pre  38870  dihord2pre  38885  dih1dimatlem0  38988  lcfrlem9  39210  remulcand  40020  prjspner1  40063  0prjspnrel  40064  nna4b4nsq  40092  rexrabdioph  40211  ctbnfien  40235  irrapxlem3  40241  elpell14qr2  40279  elpell1qr2  40289  kelac1  40483  iunrelexpuztr  40896  rfovcnvfvd  41184  radcnvrat  41493  nznngen  41495  tz6.12-afv  44228  tz6.12-afv2  44295  iccelpart  44449  prproropf1olem3  44521  lighneallem4  44626  perfectALTV  44739  bgoldbtbndlem3  44823  tgoldbach  44833  isomuspgr  44850  isassintop  44968  ellcoellss  45340  lindslinindsimp2  45368  itscnhlinecirc02plem3  45694  inlinecirc02p  45697  aacllem  45988