Theorem expr 457

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
expr	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 407	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:  animpimp2impd  844  3expia  1121  rexlimdvaa  3156  reximddv  3171  disjxiun  5145  wereu2  5673  frpomin  6341  ordtr3  6409  fcof1  7284  knatar  7353  riota5f  7393  ovmpodf  7563  extmptsuppeq  8172  suppss  8178  suppssOLD  8179  suppss2  8184  frrlem14  8283  fprresex  8294  wfrlem17OLD  8324  smoord  8364  tfrlem9a  8385  oaass  8560  oelimcl  8599  oaabs2  8647  cofon1  8670  naddssim  8683  swoso  8735  eceqoveq  8815  domdifsn  9053  domunsncan  9071  omxpenlem  9072  enfixsn  9080  mapdom2  9147  frfi  9287  fofinf1o  9326  finsschain  9358  elfiun  9424  marypha1lem  9427  eqsupd  9451  eqinfd  9479  ordiso2  9509  ordtypelem6  9517  ordtypelem7  9518  ordtypelem10  9521  oismo  9534  wemapsolem  9544  brwdom2  9567  wdomtr  9569  unwdomg  9578  xpwdomg  9579  unxpwdom2  9582  cantnfval2  9663  cantnfle  9665  cantnflem1  9683  cantnf  9687  r1ordg  9772  tcrank  9878  carddomi2  9964  harval2  9991  infxpenlem  10007  infxpenc2lem2  10014  fseqenlem1  10018  dfac8clem  10026  acndom2  10048  infpwfien  10056  iunfictbso  10108  dfac12lem3  10139  infxp  10209  coflim  10255  cofsmo  10263  coftr  10267  sornom  10271  infpssrlem4  10300  enfin2i  10315  fin23lem26  10319  fin23lem27  10322  fin23lem36  10342  fin23lem40  10345  isf32lem5  10351  isf34lem4  10371  isfin1-3  10380  fin1a2lem10  10403  fin1a2lem13  10406  fin1a2s  10408  hsmexlem4  10423  ttukeylem5  10507  ttukeylem6  10508  ttukeylem7  10509  alephval2  10566  gchor  10621  fpwwe2lem6  10630  fpwwe2lem11  10635  fpwwe2  10637  pwfseqlem4a  10655  pwfseqlem4  10656  winalim2  10690  gchina  10693  inar1  10769  nqereq  10929  prlem934  11027  prlem936  11041  addsrmo  11067  mulsrmo  11068  supsrlem  11105  axpre-sup  11163  dedekind  11376  dedekindle  11377  mulge0b  12083  supaddc  12180  supmul1  12182  un0addcl  12504  un0mulcl  12505  uzwo3  12926  qbtwnre  13177  xlemul1a  13266  seqcl2  13985  seqfveq2  13989  seqshft2  13993  monoord  13997  seqsplit  14000  seqf1olem1  14006  seqid2  14013  seqhomo  14014  expnegz  14061  expcan  14133  ltexp2  14134  discr  14202  bcval5  14277  hashbc  14411  hashf1lem2  14416  seqcoll  14424  seqcoll2  14425  wrdind  14671  wrd2ind  14672  cau3lem  15300  ello1d  15466  lo1bdd2  15467  rlimclim  15489  climrlim2  15490  rlimdm  15494  rlimcn1  15531  reccn2  15540  rlimsqzlem  15594  lo1le  15597  caucvgrlem  15618  caurcvg2  15623  summolem2  15661  zsum  15663  fsum  15665  fsumf1o  15668  sumss  15669  fsumss  15670  fsumcl2lem  15676  fsumadd  15685  fsumcom2  15719  fsum0diag2  15728  fsummulc2  15729  fsumconst  15735  fsumrelem  15752  fsumrlim  15756  fsumo1  15757  divrcnv  15797  geomulcvg  15821  mertenslem2  15830  prodmolem2  15878  zprod  15880  fprod  15884  fprodf1o  15889  prodss  15890  fprodss  15891  fprodcl2lem  15893  fprodmul  15903  fproddiv  15904  fprodconst  15921  fprodn0  15922  fprodcom2  15927  ruclem8  16179  dvds0lem  16209  dvdsnegb  16216  dvdssub2  16243  bitsf1  16386  bitsshft  16415  bezoutlem3  16482  bezoutlem4  16483  isprm5  16643  isprm6  16650  hashgcdeq  16721  modprminv  16731  modprminveq  16732  reumodprminv  16736  pcqmul  16785  pcqcl  16788  pcxnn0cl  16792  pcxcl  16793  pc2dvds  16811  pcadd  16821  pcmpt  16824  pockthg  16838  infpnlem1  16842  prmreclem5  16852  vdwlem2  16914  vdwlem9  16921  vdwlem10  16922  vdwlem12  16924  ramub  16945  0ram  16952  ramub1lem2  16959  ramub1  16960  ramcl  16961  mreexexd  17591  acsfn2  17606  iscatd  17616  catpropd  17652  setcmon  18036  pleval2i  18288  psss  18532  mgmidsssn0  18590  mhmeql  18706  frmdss2  18743  frmdup3  18747  grprcan  18857  dfgrp3lem  18920  mulgnn0ass  18989  isnsg3  19039  ghmpreima  19113  ghmeql  19114  gaorber  19171  f1omvdco2  19315  psgnunilem1  19360  psgnunilem2  19362  oddvds  19414  gexdvds  19451  sylow1lem1  19465  odcau  19471  pgpssslw  19481  sylow2alem2  19485  sylow2blem3  19489  fislw  19492  lsmmod  19542  efgredlem  19614  frgpup3  19645  gsumval3  19774  gsumzres  19776  gsumzcl2  19777  gsumzf1o  19779  gsumzaddlem  19788  gsumconst  19801  gsumzmhm  19804  gsumzoppg  19811  gsum2d2lem  19840  ablfac1eulem  19941  pgpfac1lem5  19948  ablfaclem3  19956  issubdrg  20400  lss1d  20573  lmhmeql  20665  lspextmo  20666  lspsnat  20757  lsppratlem6  20764  islbs3  20767  lbsextlem4  20773  lidl1el  20840  cnsubrg  21004  gsumfsum  21011  prmirredlem  21041  znidomb  21116  frgpcyg  21128  cssmre  21245  dsmmsubg  21297  dsmmlss  21298  frlmsslsp  21350  lindff1  21374  lindfrn  21375  rnasclassa  21448  mvrf1  21544  mplsubglem  21557  mpllsslem  21558  mplcoe1  21591  mplcoe5  21594  gsummoncoe1  21827  mat1dimcrng  21978  mdetdiaglem  22099  mdetunilem7  22119  mdetunilem8  22120  mdetunilem9  22121  cpmatacl  22217  cpmatmcllem  22219  mp2pm2mplem4  22310  en2top  22487  toponmre  22596  topssnei  22627  innei  22628  clslp  22651  restcls  22684  restntr  22685  ordtrest2lem  22706  cnpco  22770  cncls2  22776  cncnpi  22781  cncnp  22783  cnconst2  22786  cnpdis  22796  lmcnp  22807  cnhaus  22857  isreg2  22880  cncmp  22895  tgcmp  22904  sscmp  22908  cmpfi  22911  cnconn  22925  iunconnlem  22930  clsconn  22933  1stcfb  22948  1stcrest  22956  2ndcctbss  22958  2ndcdisj  22959  1stcelcls  22964  1stccnp  22965  restnlly  22985  cldllycmp  22998  lly1stc  22999  dislly  23000  locfincmp  23029  comppfsc  23035  kgentopon  23041  kgenidm  23050  1stckgenlem  23056  kgencn3  23061  ptpjpre1  23074  ptbasin  23080  txcls  23107  tx2cn  23113  ptpjcn  23114  ptclsg  23118  ptcnp  23125  txdis  23135  txlly  23139  txnlly  23140  pthaus  23141  txtube  23143  txcmplem1  23144  txcmplem2  23145  txcmp  23146  txhaus  23150  txkgen  23155  xkohaus  23156  xkococnlem  23162  xkococn  23163  txconn  23192  qtopeu  23219  qtoprest  23220  regr1lem2  23243  kqreglem1  23244  cmphaushmeo  23303  xkocnv  23317  fgabs  23382  filuni  23388  trufil  23413  ufileu  23422  filufint  23423  fin1aufil  23435  elfm2  23451  rnelfmlem  23455  fmfnfmlem2  23458  fmfnfmlem4  23460  fmufil  23462  flimopn  23478  fbflim2  23480  hausflimi  23483  hausflim  23484  flimcf  23485  flimclslem  23487  flimsncls  23489  hauspwpwf1  23490  cnpflfi  23502  fclsnei  23522  fclscf  23528  flimfnfcls  23531  fclscmp  23533  ufilcmp  23535  fcfnei  23538  cnpfcf  23544  alexsublem  23547  alexsub  23548  alexsubALTlem2  23551  alexsubALTlem3  23552  alexsubALTlem4  23553  ptcmplem3  23557  ptcmplem4  23558  ptcmplem5  23559  symgtgp  23609  tgpconncompeqg  23615  tgpconncomp  23616  ghmcnp  23618  tgpt0  23622  qustgplem  23624  haustsms2  23640  tsmsgsum  23642  tsmsres  23647  tsmsxp  23658  imasdsf1olem  23878  xbln0  23919  blssps  23929  blss  23930  neibl  24009  blcld  24013  metss  24016  metequiv2  24018  met1stc  24029  metrest  24032  prdsxmslem2  24037  metcnp3  24048  nrmmetd  24082  nlmvscnlem1  24202  nrginvrcnlem  24207  nmoleub  24247  icccmplem2  24338  icccmp  24340  reconnlem2  24342  xrge0tsms  24349  metdstri  24366  metdseq0  24369  metdscn  24371  cnmpopc  24443  lebnumlem3  24478  pcoval2  24531  pcopt  24537  nmoleub2lem  24629  nmhmcn  24635  ipcnlem1  24761  cfilfcls  24790  cmetcaulem  24804  iscmet3lem2  24808  iscmet3  24809  equivcau  24816  caubl  24824  bcthlem2  24841  bcthlem3  24842  bcthlem4  24843  bcthlem5  24844  ivthlem2  24968  ivthlem3  24969  ovoliunlem2  25019  ovolicc2lem2  25034  ovolicc2lem5  25037  ovolicc2  25038  ismbl2  25043  nulmbl  25051  nulmbl2  25052  unmbl  25053  shftmbl  25054  voliunlem3  25068  volsup  25072  ioombl1lem4  25077  ioombl1  25078  icombl  25080  ioombl  25081  uniioombl  25105  opnmbllem  25117  volivth  25123  vitali  25129  mbflimsup  25182  i1fadd  25211  itg1addlem4  25215  itg1addlem4OLD  25216  itg2le  25256  itg2seq  25259  itg2lea  25261  itg2splitlem  25265  itg2split  25266  itg2mono  25270  itg2gt0  25277  itg2cnlem2  25279  itgss  25328  itgfsum  25343  itgcn  25361  ellimc3  25395  limcco  25409  limciun  25410  dvnres  25447  dvnfre  25468  rolle  25506  c1liplem1  25512  dvivth  25526  dvne0  25527  lhop1lem  25529  lhop1  25530  lhop  25532  dvcnvrelem1  25533  dvfsumrlim  25547  dvfsum2  25550  ftc1a  25553  ftc1lem6  25557  itgsubst  25565  tdeglem4  25576  tdeglem4OLD  25577  mdegaddle  25591  mdegvscale  25592  mdegmullem  25595  deg1tmle  25634  ply1divex  25653  dvdsq1p  25677  fta1g  25684  fta1b  25686  plyco0  25705  coeeulem  25737  dgrlem  25742  plyco  25754  coemullem  25763  dgreq0  25778  dgrco  25788  plydivex  25809  quotcan  25821  aannenlem1  25840  aalioulem2  25845  aalioulem3  25846  taylthlem1  25884  ulmbdd  25909  itgulm  25919  radcnvlt1  25929  psercnlem1  25936  abelthlem2  25943  abelthlem8  25950  logcnlem5  26153  efopn  26165  cxpmul2z  26198  cxpcn3lem  26252  cxpeq  26262  xrlimcnp  26470  cxplim  26473  o1cxp  26476  cxploglim  26479  scvxcvx  26487  jensen  26490  ftalem1  26574  ftalem2  26575  fta  26581  basellem3  26584  isppw2  26616  ppinprm  26653  chtnprm  26655  dvdsmulf1o  26695  chtublem  26711  perfectlem2  26730  dchrfi  26755  dchrptlem1  26764  dchrptlem2  26765  dchrptlem3  26766  dchrsum2  26768  bposlem1  26784  bposlem3  26786  2sqlem5  26922  2sqlem6  26923  2sqlem8  26926  2sqlem10  26928  2sqb  26932  chebbnd1lem1  26969  chtppilimlem2  26974  dchrisum0flb  27010  dchrisum0fno1  27011  dchrisum0  27020  pntrsumbnd2  27067  pntpbnd1  27086  pntpbnd2  27087  pntlemp  27110  pnt3  27112  qabvle  27125  ostth2lem2  27134  ostth3  27138  ostth  27139  nolt02o  27195  nogt01o  27196  nosupprefixmo  27200  noinfprefixmo  27201  nosupbnd1lem3  27210  nosupbnd1lem4  27211  nosupbnd1lem5  27212  noinfbnd1lem3  27225  noinfbnd1lem4  27226  noinfbnd1lem5  27227  noetasuplem4  27236  noetainflem4  27240  etasslt  27311  cuteq1  27331  madebdaylemlrcut  27390  cutlt  27416  mulsuniflem  27601  colinearalglem4  28164  axcontlem10  28228  upgrex  28349  smcnlem  29945  ubthlem1  30118  ubthlem3  30120  htthlem  30165  5oalem6  30907  leopmuli  31381  pjnormssi  31416  pjclem4  31447  pj3si  31455  hatomistici  31610  sumdmdlem  31666  wrdt2ind  32112  xrge0tsmsd  32204  isarchiofld  32430  ordtrest2NEWlem  32897  qqhf  32961  eulerpartlemb  33362  ballotlemfc0  33486  ballotlemfcc  33487  sgn3da  33535  subfacp1lem5  34170  erdszelem7  34183  erdszelem11  34187  pconnconn  34217  txpconn  34218  connpconn  34221  sconnpi1  34225  txsconn  34227  cvxsconn  34229  cvmopnlem  34264  cvmfolem  34265  cvmliftmolem2  34268  cvmliftlem7  34277  cvmliftlem10  34280  cvmlift2lem10  34298  cvmlift3lem4  34308  cvmlift3lem8  34312  satfun  34397  msubff1  34542  wzel  34791  wsuclem  34792  btwnouttr2  34989  cgrxfr  35022  btwnxfr  35023  brcolinear  35026  lineext  35043  btwnconn1lem13  35066  midofsegid  35071  segcon2  35072  brsegle  35075  seglecgr12im  35077  segletr  35081  colinbtwnle  35085  broutsideof2  35089  btwnoutside  35092  broutsideof3  35093  outsideoftr  35096  outsideofeq  35097  outsideofeu  35098  outsidele  35099  lineunray  35114  lineelsb2  35115  linethru  35120  finminlem  35198  nn0prpwlem  35202  neibastop2lem  35240  neibastop2  35241  neibastop3  35242  topjoin  35245  tailfb  35257  relowlssretop  36239  fvineqsneq  36288  wl-sbcom2d-lem1  36419  finixpnum  36468  poimirlem6  36489  poimirlem7  36490  poimirlem13  36496  poimirlem26  36509  poimirlem29  36512  heicant  36518  opnmbllem0  36519  mblfinlem3  36522  ismblfin  36524  ovoliunnfl  36525  voliunnfl  36527  volsupnfl  36528  itg2addnclem  36534  itg2addnclem3  36536  ftc1cnnc  36555  sdclem2  36605  fdc  36608  istotbnd3  36634  isbnd2  36646  isbnd3  36647  prdsbnd  36656  cntotbnd  36659  heibor1lem  36672  heibor1  36673  heiborlem10  36683  rrncmslem  36695  ghomco  36754  1idl  36889  unichnidl  36894  disjlem18  37665  prtlem10  37730  prtlem18  37742  atlatmstc  38184  cvrexchlem  38285  paddasslem14  38699  pexmidlem5N  38840  cdleme29ex  39240  cdlemefr29exN  39268  cdleme32fva  39303  diarnN  39995  dihlsscpre  40100  isnacs3  41438  fnwe2lem2  41783  kelac1  41795  hbtlem5  41860  hbt  41862  dgraa0p  41881  ofoafg  42094  ofoafo  42096  naddcnffo  42104  fzunt  42196  fzuntd  42197  monoordxrv  44182  rlimdmafv  45875  rlimdmafv2  45956  fmtnoprmfac2  46225  perfectALTVlem2  46380  mogoldbb  46443  mgmhmeql  46563  lindslinindsimp2  47134