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  3196  vtoclgft  3510  moi2  3675  preq12bg  4810  disjxiun  5096  disjxun  5097  wereu2  5622  frpomin  6299  f1ocnv2d  7613  funeldmdif  7994  extmptsuppeq  8132  suppssr  8139  suppssrg  8140  omeulem1  8511  oelim2  8525  oeoa  8527  boxriin  8882  frfi  9189  fipreima  9262  marypha1lem  9340  supiso  9383  ordtypelem10  9436  r1ordg  9694  infxpenc2lem1  9933  acndom  9965  acndom2  9968  cofsmo  10183  cfcoflem  10186  fin23lem28  10254  fin23lem36  10262  isf32lem1  10267  isf32lem2  10268  isf32lem5  10271  isf34lem4  10291  fin1a2lem6  10319  fin1a2s  10328  ttukeylem2  10424  ttukeylem6  10428  fpwwe2lem7  10552  fpwwe2lem11  10556  inar1  10690  grudomon  10732  axpre-sup  11084  un0addcl  12438  un0mulcl  12439  peano2uz2  12584  rpnnen1lem2  12894  rpnnen1lem1  12895  rpnnen1lem3  12896  rpnnen1lem5  12898  xlemul1a  13207  fzadd2  13479  elfz2nn0  13538  fzind2  13708  expaddz  14033  expmulz  14035  swrdswrd  14632  cau3lem  15282  lo1bdd2  15451  climuni  15479  fsumcom2  15701  fprodcom2  15911  dvdsval2  16186  algcvga  16510  lcmgcdlem  16537  coprmproddvdslem  16593  divgcdcoprmex  16597  iserodd  16767  prmpwdvds  16836  ram0  16954  catpropd  17636  mndind  18757  isgrpinv  18927  gicsubgen  19212  sylow2alem2  19551  sylow2a  19552  frgpuptinv  19704  gsumcom3fi  19912  gsumxp2  19913  ablfac1eu  20008  dvdsrcl2  20306  islss4  20917  ellspsn6  20949  lmhmima  21003  lsmcl  21039  psgnodpm  21547  dsmmlss  21703  islindf4  21797  gsumbagdiag  21891  psrass1lem  21892  coe1tmmul2  22222  dmatscmcl  22451  mdetdiaglem  22546  mdetunilem9  22568  pm2mp  22773  epttop  22957  neindisj  23065  neitr  23128  restcls  23129  restntr  23130  ordtrest2lem  23151  cncnp  23228  cnconst  23232  1stcrest  23401  2ndcdisj  23404  2ndcsep  23407  1stccnp  23410  islly2  23432  1stckgenlem  23501  ptbasin  23525  ptbasfi  23529  ptcnplem  23569  ptcnp  23570  tx1stc  23598  qtophmeo  23765  filconn  23831  filuni  23833  ufileu  23867  elfm3  23898  rnelfmlem  23900  fmfnfmlem4  23905  cnpflf2  23948  alexsubALTlem4  23998  ptcmplem3  24002  ptcmplem4  24003  ptcmplem5  24004  tsmsxplem1  24101  bl2in  24348  metcnpi  24492  metcnpi2  24493  metcnpi3  24494  recld2  24763  icoopnst  24896  iocopnst  24897  ncvs1  25117  iscfil3  25233  iscmet3lem2  25252  ovoliunlem1  25463  ovolicc2lem2  25479  ovolicc2lem4  25481  voliun  25515  volsuplem  25516  dyadmbllem  25560  mbfinf  25626  mbflimsup  25627  itg2seq  25703  itg2splitlem  25709  itg2cnlem1  25722  ellimc3  25840  dvnadd  25891  dvcnvlem  25940  c1liplem1  25961  lhop2  25980  coe1mul3  26064  ply1divex  26102  dvdsq1p  26128  aannenlem1  26296  aalioulem2  26301  dvtaylp  26338  ulmdvlem3  26371  iblulm  26376  cxpmul2z  26660  xrlimcnp  26938  lgambdd  27007  wilthlem2  27039  basellem3  27053  dvdsflsumcom  27158  perfect  27202  dchreq  27229  dchrsum  27240  bposlem1  27255  lgsquad2  27357  dchrisum0fno1  27482  pntibnd  27564  noinfbnd1lem4  27698  cuteq1  27817  madebdaylemlrcut  27899  precsexlem11  28217  recsex  28219  bdayons  28276  addonbday  28279  noseqp1  28291  noseqrdgfn  28306  bdaypw2n0bndlem  28463  bdayfinbndlem1  28467  remulscllem2  28501  oppperpex  28829  lmieu  28860  ax5seglem5  29010  axeuclid  29040  egrsubgr  29354  nbumgrvtx  29423  wwlksnextsurj  29977  clwwlkccat  30069  numclwwlk2lem1lem  30421  nmcvcn  30774  ubthlem1  30949  leopmul2i  32214  hstel2  32298  atom1d  32432  cdj1i  32512  f1o3d  32707  fsuppcurry1  32805  fsuppcurry2  32806  xrge0addge  32840  isdrng4  33379  prmidl0  33533  mxidlmax  33548  reff  33998  ordtrest2NEWlem  34081  esumcst  34222  eulerpartlemgh  34537  cvmscld  35469  cgrxfr  36251  finminlem  36514  nn0prpwlem  36518  neibastop1  36555  neibastop2lem  36556  tailfb  36573  fvineqsneu  37618  pibt2  37624  finixpnum  37808  lindsenlbs  37818  matunitlindflem2  37820  poimirlem4  37827  poimirlem25  37848  poimirlem26  37849  poimirlem29  37852  poimirlem30  37853  poimirlem31  37854  poimirlem32  37855  heicant  37858  mblfinlem3  37862  mblfinlem4  37863  itg2addnclem  37874  itg2addnclem3  37876  ftc1anc  37904  subspopn  37955  prdsbnd  37996  heibor1lem  38012  heiborlem1  38014  heibor  38024  isdrngo2  38161  rngoisocnv  38184  maxidlmax  38246  riotasv3d  39288  lkrpssN  39491  intnatN  39735  elpaddatiN  40133  pexmidlem5N  40302  lhpj1  40350  ltrnu  40449  cdlemn11pre  41538  dihord2pre  41553  dih1dimatlem0  41656  lcfrlem9  41878  remulcand  42761  prjspner1  42936  0prjspnrel  42937  nna4b4nsq  42970  rexrabdioph  43103  ctbnfien  43127  irrapxlem3  43133  elpell14qr2  43171  elpell1qr2  43181  kelac1  43372  iunrelexpuztr  44027  rfovcnvfvd  44315  radcnvrat  44622  nznngen  44624  tz6.12-afv  47486  tz6.12-afv2  47553  iccelpart  47746  prproropf1olem3  47818  lighneallem4  47923  perfectALTV  48036  bgoldbtbndlem3  48120  tgoldbach  48130  grimcnv  48201  grimco  48202  isuspgrim0  48207  grimedg  48248  isubgr3stgrlem7  48285  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem3  48386  isassintop  48523  ellcoellss  48748  lindslinindsimp2  48776  itscnhlinecirc02plem3  49097  inlinecirc02p  49100  aacllem  50113