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  3515  moi2  3684  preq12bg  4813  disjxiun  5099  disjxun  5100  wereu2  5628  frpomin  6301  f1ocnv2d  7622  funeldmdif  8006  extmptsuppeq  8144  suppssr  8151  suppssrg  8152  omeulem1  8523  oelim2  8536  oeoa  8538  boxriin  8890  frfi  9208  fipreima  9285  marypha1lem  9360  supiso  9403  ordtypelem10  9456  r1ordg  9707  infxpenc2lem1  9948  acndom  9980  acndom2  9983  cofsmo  10198  cfcoflem  10201  fin23lem28  10269  fin23lem36  10277  isf32lem1  10282  isf32lem2  10283  isf32lem5  10286  isf34lem4  10306  fin1a2lem6  10334  fin1a2s  10343  ttukeylem2  10439  ttukeylem6  10443  fpwwe2lem7  10566  fpwwe2lem11  10570  inar1  10704  grudomon  10746  axpre-sup  11098  un0addcl  12451  un0mulcl  12452  peano2uz2  12598  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  xlemul1a  13224  fzadd2  13496  elfz2nn0  13555  fzind2  13722  expaddz  14047  expmulz  14049  swrdswrd  14646  cau3lem  15297  lo1bdd2  15466  climuni  15494  fsumcom2  15716  fprodcom2  15926  dvdsval2  16201  algcvga  16525  lcmgcdlem  16552  coprmproddvdslem  16608  divgcdcoprmex  16612  iserodd  16782  prmpwdvds  16851  ram0  16969  catpropd  17650  mndind  18737  isgrpinv  18907  gicsubgen  19193  sylow2alem2  19532  sylow2a  19533  frgpuptinv  19685  gsumcom3fi  19893  gsumxp2  19894  ablfac1eu  19989  dvdsrcl2  20286  islss4  20900  ellspsn6  20932  lmhmima  20986  lsmcl  21022  psgnodpm  21530  dsmmlss  21686  islindf4  21780  gsumbagdiag  21873  psrass1lem  21874  coe1tmmul2  22195  dmatscmcl  22423  mdetdiaglem  22518  mdetunilem9  22540  pm2mp  22745  epttop  22929  neindisj  23037  neitr  23100  restcls  23101  restntr  23102  ordtrest2lem  23123  cncnp  23200  cnconst  23204  1stcrest  23373  2ndcdisj  23376  2ndcsep  23379  1stccnp  23382  islly2  23404  1stckgenlem  23473  ptbasin  23497  ptbasfi  23501  ptcnplem  23541  ptcnp  23542  tx1stc  23570  qtophmeo  23737  filconn  23803  filuni  23805  ufileu  23839  elfm3  23870  rnelfmlem  23872  fmfnfmlem4  23877  cnpflf2  23920  alexsubALTlem4  23970  ptcmplem3  23974  ptcmplem4  23975  ptcmplem5  23976  tsmsxplem1  24073  bl2in  24321  metcnpi  24465  metcnpi2  24466  metcnpi3  24467  recld2  24736  icoopnst  24869  iocopnst  24870  ncvs1  25090  iscfil3  25206  iscmet3lem2  25225  ovoliunlem1  25436  ovolicc2lem2  25452  ovolicc2lem4  25454  voliun  25488  volsuplem  25489  dyadmbllem  25533  mbfinf  25599  mbflimsup  25600  itg2seq  25676  itg2splitlem  25682  itg2cnlem1  25695  ellimc3  25813  dvnadd  25864  dvcnvlem  25913  c1liplem1  25934  lhop2  25953  coe1mul3  26037  ply1divex  26075  dvdsq1p  26101  aannenlem1  26269  aalioulem2  26274  dvtaylp  26311  ulmdvlem3  26344  iblulm  26349  cxpmul2z  26633  xrlimcnp  26911  lgambdd  26980  wilthlem2  27012  basellem3  27026  dvdsflsumcom  27131  perfect  27175  dchreq  27202  dchrsum  27213  bposlem1  27228  lgsquad2  27330  dchrisum0fno1  27455  pntibnd  27537  noinfbnd1lem4  27671  cuteq1  27783  madebdaylemlrcut  27848  precsexlem11  28159  recsex  28161  bdayon  28213  noseqp1  28225  noseqrdgfn  28240  remulscllem2  28405  oppperpex  28733  lmieu  28764  ax5seglem5  28913  axeuclid  28943  egrsubgr  29257  nbumgrvtx  29326  wwlksnextsurj  29880  clwwlkccat  29969  numclwwlk2lem1lem  30321  nmcvcn  30674  ubthlem1  30849  leopmul2i  32114  hstel2  32198  atom1d  32332  cdj1i  32412  f1o3d  32601  fsuppcurry1  32698  fsuppcurry2  32699  xrge0addge  32731  isdrng4  33261  prmidl0  33414  mxidlmax  33429  reff  33822  ordtrest2NEWlem  33905  esumcst  34046  eulerpartlemgh  34362  cvmscld  35253  cgrxfr  36036  finminlem  36299  nn0prpwlem  36303  neibastop1  36340  neibastop2lem  36341  tailfb  36358  fvineqsneu  37392  pibt2  37398  finixpnum  37592  lindsenlbs  37602  matunitlindflem2  37604  poimirlem4  37611  poimirlem25  37632  poimirlem26  37633  poimirlem29  37636  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  heicant  37642  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem  37658  itg2addnclem3  37660  ftc1anc  37688  subspopn  37739  prdsbnd  37780  heibor1lem  37796  heiborlem1  37798  heibor  37808  isdrngo2  37945  rngoisocnv  37968  maxidlmax  38030  riotasv3d  38946  lkrpssN  39149  intnatN  39394  elpaddatiN  39792  pexmidlem5N  39961  lhpj1  40009  ltrnu  40108  cdlemn11pre  41197  dihord2pre  41212  dih1dimatlem0  41315  lcfrlem9  41537  remulcand  42420  prjspner1  42607  0prjspnrel  42608  nna4b4nsq  42641  rexrabdioph  42775  ctbnfien  42799  irrapxlem3  42805  elpell14qr2  42843  elpell1qr2  42853  kelac1  43045  iunrelexpuztr  43701  rfovcnvfvd  43989  radcnvrat  44296  nznngen  44298  tz6.12-afv  47167  tz6.12-afv2  47234  iccelpart  47427  prproropf1olem3  47499  lighneallem4  47604  perfectALTV  47717  bgoldbtbndlem3  47801  tgoldbach  47811  grimcnv  47881  grimco  47882  isuspgrim0  47887  grimedg  47928  isubgr3stgrlem7  47964  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem3  48057  isassintop  48191  ellcoellss  48417  lindslinindsimp2  48445  itscnhlinecirc02plem3  48766  inlinecirc02p  48769  aacllem  49783