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  3211  moi2  3708  preq12bg  4847  disjxiun  5138  disjxun  5139  wereu2  5666  frpomin  6330  f1ocnv2d  7642  funeldmdif  8016  extmptsuppeq  8155  suppssr  8163  suppssrg  8164  omeulem1  8565  oelim2  8578  oeoa  8580  boxriin  8917  frfi  9271  fipreima  9341  marypha1lem  9410  supiso  9452  ordtypelem10  9504  r1ordg  9755  infxpenc2lem1  9996  acndom  10028  acndom2  10031  cofsmo  10246  cfcoflem  10249  fin23lem28  10317  fin23lem36  10325  isf32lem1  10330  isf32lem2  10331  isf32lem5  10334  isf34lem4  10354  fin1a2lem6  10382  fin1a2s  10391  ttukeylem2  10487  ttukeylem6  10491  fpwwe2lem7  10614  fpwwe2lem11  10618  inar1  10752  grudomon  10794  axpre-sup  11146  un0addcl  12487  un0mulcl  12488  peano2uz2  12632  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  xlemul1a  13249  fzadd2  13518  elfz2nn0  13574  fzind2  13732  expaddz  14054  expmulz  14056  swrdswrd  14637  cau3lem  15283  lo1bdd2  15450  climuni  15478  fsumcom2  15702  fprodcom2  15910  dvdsval2  16182  algcvga  16498  lcmgcdlem  16525  coprmproddvdslem  16581  divgcdcoprmex  16585  iserodd  16750  prmpwdvds  16819  ram0  16937  catpropd  17635  mndind  18684  isgrpinv  18853  gicsubgen  19118  sylow2alem2  19450  sylow2a  19451  frgpuptinv  19603  gsumcom3fi  19806  gsumxp2  19807  ablfac1eu  19902  dvdsrcl2  20132  islss4  20522  lspsnel6  20554  lmhmima  20607  lsmcl  20643  psgnodpm  21074  dsmmlss  21232  islindf4  21326  gsumbagdiagOLD  21423  psrass1lemOLD  21424  gsumbagdiag  21426  psrass1lem  21427  coe1tmmul2  21729  dmatscmcl  21934  mdetdiaglem  22029  mdetunilem9  22051  pm2mp  22256  epttop  22441  neindisj  22550  neitr  22613  restcls  22614  restntr  22615  ordtrest2lem  22636  cncnp  22713  cnconst  22717  1stcrest  22886  2ndcdisj  22889  2ndcsep  22892  1stccnp  22895  islly2  22917  1stckgenlem  22986  ptbasin  23010  ptbasfi  23014  ptcnplem  23054  ptcnp  23055  tx1stc  23083  qtophmeo  23250  filconn  23316  filuni  23318  ufileu  23352  elfm3  23383  rnelfmlem  23385  fmfnfmlem4  23390  cnpflf2  23433  alexsubALTlem4  23483  ptcmplem3  23487  ptcmplem4  23488  ptcmplem5  23489  tsmsxplem1  23586  bl2in  23835  metcnpi  23982  metcnpi2  23983  metcnpi3  23984  recld2  24259  icoopnst  24384  iocopnst  24385  ncvs1  24603  iscfil3  24719  iscmet3lem2  24738  ovoliunlem1  24948  ovolicc2lem2  24964  ovolicc2lem4  24966  voliun  25000  volsuplem  25001  dyadmbllem  25045  mbfinf  25111  mbflimsup  25112  itg2seq  25189  itg2splitlem  25195  itg2cnlem1  25208  ellimc3  25325  dvnadd  25375  dvcnvlem  25422  c1liplem1  25442  lhop2  25461  coe1mul3  25546  ply1divex  25583  dvdsq1p  25607  aannenlem1  25770  aalioulem2  25775  dvtaylp  25811  ulmdvlem3  25843  iblulm  25848  cxpmul2z  26128  xrlimcnp  26400  lgambdd  26468  wilthlem2  26500  basellem3  26514  dvdsflsumcom  26619  perfect  26661  dchreq  26688  dchrsum  26699  bposlem1  26714  lgsquad2  26816  dchrisum0fno1  26941  pntibnd  27023  noinfbnd1lem4  27156  madebdaylemlrcut  27316  oppperpex  27869  lmieu  27900  ax5seglem5  28056  axeuclid  28086  egrsubgr  28399  nbumgrvtx  28468  wwlksnextsurj  29019  clwwlkccat  29108  numclwwlk2lem1lem  29460  nmcvcn  29811  ubthlem1  29986  leopmul2i  31251  hstel2  31335  atom1d  31469  cdj1i  31549  f1o3d  31719  fsuppcurry1  31821  fsuppcurry2  31822  xrge0addge  31841  isdrng4  32257  prmidl0  32418  mxidlmax  32430  reff  32648  ordtrest2NEWlem  32731  esumcst  32890  eulerpartlemgh  33206  cvmscld  34093  cgrxfr  34855  finminlem  35005  nn0prpwlem  35009  neibastop1  35046  neibastop2lem  35047  tailfb  35064  fvineqsneu  36094  pibt2  36100  finixpnum  36275  lindsenlbs  36285  matunitlindflem2  36287  poimirlem4  36294  poimirlem25  36315  poimirlem26  36316  poimirlem29  36319  poimirlem30  36320  poimirlem31  36321  poimirlem32  36322  heicant  36325  mblfinlem3  36329  mblfinlem4  36330  itg2addnclem  36341  itg2addnclem3  36343  ftc1anc  36371  subspopn  36423  prdsbnd  36464  heibor1lem  36480  heiborlem1  36482  heibor  36492  isdrngo2  36629  rngoisocnv  36652  maxidlmax  36714  riotasv3d  37633  lkrpssN  37836  intnatN  38081  elpaddatiN  38479  pexmidlem5N  38648  lhpj1  38696  ltrnu  38795  cdlemn11pre  39884  dihord2pre  39899  dih1dimatlem0  40002  lcfrlem9  40224  remulcand  41091  prjspner1  41148  0prjspnrel  41149  nna4b4nsq  41182  rexrabdioph  41301  ctbnfien  41325  irrapxlem3  41331  elpell14qr2  41369  elpell1qr2  41379  kelac1  41574  iunrelexpuztr  42239  rfovcnvfvd  42527  radcnvrat  42842  nznngen  42844  tz6.12-afv  45651  tz6.12-afv2  45718  iccelpart  45871  prproropf1olem3  45943  lighneallem4  46048  perfectALTV  46161  bgoldbtbndlem3  46245  tgoldbach  46255  isomuspgr  46272  isassintop  46390  ellcoellss  46762  lindslinindsimp2  46790  itscnhlinecirc02plem3  47116  inlinecirc02p  47119  aacllem  47494