Theorem expr 456

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 406	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:  animpimp2impd  846  3expia  1121  rexlimdvaa  3136  reximddv  3150  disjxiun  5106  wereu2  5637  frpomin  6315  ordtr3  6380  fcof1  7264  knatar  7334  riota5f  7374  ovmpodf  7547  extmptsuppeq  8169  suppss  8175  suppss2  8181  frrlem14  8280  fprresex  8291  smoord  8336  tfrlem9a  8356  oaass  8527  oelimcl  8566  oaabs2  8615  cofon1  8638  naddssim  8651  swoso  8707  eceqoveq  8797  domdifsn  9027  domunsncan  9045  omxpenlem  9046  enfixsn  9054  mapdom2  9117  frfi  9238  fofinf1o  9289  finsschain  9316  elfiun  9387  marypha1lem  9390  eqsupd  9414  eqinfd  9443  ordiso2  9474  ordtypelem6  9482  ordtypelem7  9483  ordtypelem10  9486  oismo  9499  wemapsolem  9509  brwdom2  9532  wdomtr  9534  unwdomg  9543  xpwdomg  9544  unxpwdom2  9547  cantnfval2  9628  cantnfle  9630  cantnflem1  9648  cantnf  9652  r1ordg  9737  tcrank  9843  carddomi2  9929  harval2  9956  infxpenlem  9972  infxpenc2lem2  9979  fseqenlem1  9983  dfac8clem  9991  acndom2  10013  infpwfien  10021  iunfictbso  10073  dfac12lem3  10105  infxp  10173  coflim  10220  cofsmo  10228  coftr  10232  sornom  10236  infpssrlem4  10265  enfin2i  10280  fin23lem26  10284  fin23lem27  10287  fin23lem36  10307  fin23lem40  10310  isf32lem5  10316  isf34lem4  10336  isfin1-3  10345  fin1a2lem10  10368  fin1a2lem13  10371  fin1a2s  10373  hsmexlem4  10388  ttukeylem5  10472  ttukeylem6  10473  ttukeylem7  10474  alephval2  10531  gchor  10586  fpwwe2lem6  10595  fpwwe2lem11  10600  fpwwe2  10602  pwfseqlem4a  10620  pwfseqlem4  10621  winalim2  10655  gchina  10658  inar1  10734  nqereq  10894  prlem934  10992  prlem936  11006  addsrmo  11032  mulsrmo  11033  supsrlem  11070  axpre-sup  11128  dedekind  11343  dedekindle  11344  mulge0b  12059  supaddc  12156  supmul1  12158  un0addcl  12481  un0mulcl  12482  uzwo3  12908  qbtwnre  13165  xlemul1a  13254  seqcl2  13991  seqfveq2  13995  seqshft2  13999  monoord  14003  seqsplit  14006  seqf1olem1  14012  seqid2  14019  seqhomo  14020  expnegz  14067  expcan  14140  ltexp2  14141  discr  14211  bcval5  14289  hashbc  14424  hashf1lem2  14427  seqcoll  14435  seqcoll2  14436  wrdind  14693  wrd2ind  14694  cau3lem  15327  ello1d  15495  lo1bdd2  15496  rlimclim  15518  climrlim2  15519  rlimdm  15523  rlimcn1  15560  reccn2  15569  rlimsqzlem  15621  lo1le  15624  caucvgrlem  15645  caurcvg2  15650  summolem2  15688  zsum  15690  fsum  15692  fsumf1o  15695  sumss  15696  fsumss  15697  fsumcl2lem  15703  fsumadd  15712  fsumcom2  15746  fsum0diag2  15755  fsummulc2  15756  fsumconst  15762  fsumrelem  15779  fsumrlim  15783  fsumo1  15784  divrcnv  15824  geomulcvg  15848  mertenslem2  15857  prodmolem2  15907  zprod  15909  fprod  15913  fprodf1o  15918  prodss  15919  fprodss  15920  fprodcl2lem  15922  fprodmul  15932  fproddiv  15933  fprodconst  15950  fprodn0  15951  fprodcom2  15956  ruclem8  16211  dvds0lem  16242  dvdsnegb  16249  dvdssub2  16277  bitsf1  16422  bitsshft  16451  bezoutlem3  16517  bezoutlem4  16518  isprm5  16683  isprm6  16690  hashgcdeq  16766  modprminv  16776  modprminveq  16777  reumodprminv  16781  pcqmul  16830  pcqcl  16833  pcxnn0cl  16837  pcxcl  16838  pc2dvds  16856  pcadd  16866  pcmpt  16869  pockthg  16883  infpnlem1  16887  prmreclem5  16897  vdwlem2  16959  vdwlem9  16966  vdwlem10  16967  vdwlem12  16969  ramub  16990  0ram  16997  ramub1lem2  17004  ramub1  17005  ramcl  17006  mreexexd  17615  acsfn2  17630  iscatd  17640  catpropd  17676  setcmon  18055  pleval2i  18301  psss  18545  mgmidsssn0  18605  mgmhmeql  18649  mhmeql  18759  frmdss2  18796  frmdup3  18800  grprcan  18911  dfgrp3lem  18976  mulgnn0ass  19048  isnsg3  19098  ghmpreima  19176  ghmeql  19177  gaorber  19246  f1omvdco2  19384  psgnunilem1  19429  psgnunilem2  19431  oddvds  19483  gexdvds  19520  sylow1lem1  19534  odcau  19540  pgpssslw  19550  sylow2alem2  19554  sylow2blem3  19558  fislw  19561  lsmmod  19611  efgredlem  19683  frgpup3  19714  gsumval3  19843  gsumzres  19845  gsumzcl2  19846  gsumzf1o  19848  gsumzaddlem  19857  gsumconst  19870  gsumzmhm  19873  gsumzoppg  19880  gsum2d2lem  19909  ablfac1eulem  20010  pgpfac1lem5  20017  ablfaclem3  20025  issubdrg  20695  lss1d  20875  lmhmeql  20968  lspextmo  20969  lspsnat  21061  lsppratlem6  21068  islbs3  21071  lbsextlem4  21077  lidl1el  21142  cnsubrg  21350  gsumfsum  21357  prmirredlem  21388  znidomb  21477  frgpcyg  21489  cssmre  21608  dsmmsubg  21658  dsmmlss  21659  frlmsslsp  21711  lindff1  21735  lindfrn  21736  rnasclassa  21810  mvrf1  21901  mplsubglem  21914  mpllsslem  21915  mplcoe1  21950  mplcoe5  21953  gsummoncoe1  22201  mat1dimcrng  22370  mdetdiaglem  22491  mdetunilem7  22511  mdetunilem8  22512  mdetunilem9  22513  cpmatacl  22609  cpmatmcllem  22611  mp2pm2mplem4  22702  en2top  22878  toponmre  22986  topssnei  23017  innei  23018  clslp  23041  restcls  23074  restntr  23075  ordtrest2lem  23096  cnpco  23160  cncls2  23166  cncnpi  23171  cncnp  23173  cnconst2  23176  cnpdis  23186  lmcnp  23197  cnhaus  23247  isreg2  23270  cncmp  23285  tgcmp  23294  sscmp  23298  cmpfi  23301  cnconn  23315  iunconnlem  23320  clsconn  23323  1stcfb  23338  1stcrest  23346  2ndcctbss  23348  2ndcdisj  23349  1stcelcls  23354  1stccnp  23355  restnlly  23375  cldllycmp  23388  lly1stc  23389  dislly  23390  locfincmp  23419  comppfsc  23425  kgentopon  23431  kgenidm  23440  1stckgenlem  23446  kgencn3  23451  ptpjpre1  23464  ptbasin  23470  txcls  23497  tx2cn  23503  ptpjcn  23504  ptclsg  23508  ptcnp  23515  txdis  23525  txlly  23529  txnlly  23530  pthaus  23531  txtube  23533  txcmplem1  23534  txcmplem2  23535  txcmp  23536  txhaus  23540  txkgen  23545  xkohaus  23546  xkococnlem  23552  xkococn  23553  txconn  23582  qtopeu  23609  qtoprest  23610  regr1lem2  23633  kqreglem1  23634  cmphaushmeo  23693  xkocnv  23707  fgabs  23772  filuni  23778  trufil  23803  ufileu  23812  filufint  23813  fin1aufil  23825  elfm2  23841  rnelfmlem  23845  fmfnfmlem2  23848  fmfnfmlem4  23850  fmufil  23852  flimopn  23868  fbflim2  23870  hausflimi  23873  hausflim  23874  flimcf  23875  flimclslem  23877  flimsncls  23879  hauspwpwf1  23880  cnpflfi  23892  fclsnei  23912  fclscf  23918  flimfnfcls  23921  fclscmp  23923  ufilcmp  23925  fcfnei  23928  cnpfcf  23934  alexsublem  23937  alexsub  23938  alexsubALTlem2  23941  alexsubALTlem3  23942  alexsubALTlem4  23943  ptcmplem3  23947  ptcmplem4  23948  ptcmplem5  23949  symgtgp  23999  tgpconncompeqg  24005  tgpconncomp  24006  ghmcnp  24008  tgpt0  24012  qustgplem  24014  haustsms2  24030  tsmsgsum  24032  tsmsres  24037  tsmsxp  24048  imasdsf1olem  24267  xbln0  24308  blssps  24318  blss  24319  neibl  24395  blcld  24399  metss  24402  metequiv2  24404  met1stc  24415  metrest  24418  prdsxmslem2  24423  metcnp3  24434  nrmmetd  24468  nlmvscnlem1  24580  nrginvrcnlem  24585  nmoleub  24625  icccmplem2  24718  icccmp  24720  reconnlem2  24722  xrge0tsms  24729  metdstri  24746  metdseq0  24749  metdscn  24751  cnmpopc  24828  lebnumlem3  24868  pcoval2  24922  pcopt  24928  nmoleub2lem  25020  nmhmcn  25026  ipcnlem1  25151  cfilfcls  25180  cmetcaulem  25194  iscmet3lem2  25198  iscmet3  25199  equivcau  25206  caubl  25214  bcthlem2  25231  bcthlem3  25232  bcthlem4  25233  bcthlem5  25234  ivthlem2  25359  ivthlem3  25360  ovoliunlem2  25410  ovolicc2lem2  25425  ovolicc2lem5  25428  ovolicc2  25429  ismbl2  25434  nulmbl  25442  nulmbl2  25443  unmbl  25444  shftmbl  25445  voliunlem3  25459  volsup  25463  ioombl1lem4  25468  ioombl1  25469  icombl  25471  ioombl  25472  uniioombl  25496  opnmbllem  25508  volivth  25514  vitali  25520  mbflimsup  25573  i1fadd  25602  itg1addlem4  25606  itg2le  25646  itg2seq  25649  itg2lea  25651  itg2splitlem  25655  itg2split  25656  itg2mono  25660  itg2gt0  25667  itg2cnlem2  25669  itgss  25719  itgfsum  25734  itgcn  25752  ellimc3  25786  limcco  25800  limciun  25801  dvnres  25839  dvnfre  25862  rolle  25900  c1liplem1  25907  dvivth  25921  dvne0  25922  lhop1lem  25924  lhop1  25925  lhop  25927  dvcnvrelem1  25928  dvfsumrlim  25944  dvfsum2  25947  ftc1a  25950  ftc1lem6  25954  itgsubst  25962  tdeglem4  25971  mdegaddle  25985  mdegvscale  25986  mdegmullem  25989  deg1tmle  26029  ply1divex  26048  dvdsq1p  26074  fta1g  26081  fta1b  26083  plyco0  26103  coeeulem  26135  dgrlem  26140  plyco  26152  coemullem  26161  dgreq0  26177  dgrco  26187  plydivex  26211  quotcan  26223  aannenlem1  26242  aalioulem2  26247  aalioulem3  26248  taylthlem1  26287  ulmbdd  26313  itgulm  26323  radcnvlt1  26333  psercnlem1  26341  abelthlem2  26348  abelthlem8  26355  logcnlem5  26561  efopn  26573  cxpmul2z  26606  cxpcn3lem  26663  cxpeq  26673  xrlimcnp  26884  cxplim  26888  o1cxp  26891  cxploglim  26894  scvxcvx  26902  jensen  26905  ftalem1  26989  ftalem2  26990  fta  26996  basellem3  26999  isppw2  27031  ppinprm  27068  chtnprm  27070  mpodvdsmulf1o  27110  dvdsmulf1o  27112  chtublem  27128  perfectlem2  27147  dchrfi  27172  dchrptlem1  27181  dchrptlem2  27182  dchrptlem3  27183  dchrsum2  27185  bposlem1  27201  bposlem3  27203  2sqlem5  27339  2sqlem6  27340  2sqlem8  27343  2sqlem10  27345  2sqb  27349  chebbnd1lem1  27386  chtppilimlem2  27391  dchrisum0flb  27427  dchrisum0fno1  27428  dchrisum0  27437  pntrsumbnd2  27484  pntpbnd1  27503  pntpbnd2  27504  pntlemp  27527  pnt3  27529  qabvle  27542  ostth2lem2  27551  ostth3  27555  ostth  27556  nolt02o  27613  nogt01o  27614  nosupprefixmo  27618  noinfprefixmo  27619  nosupbnd1lem3  27628  nosupbnd1lem4  27629  nosupbnd1lem5  27630  noinfbnd1lem3  27643  noinfbnd1lem4  27644  noinfbnd1lem5  27645  noetasuplem4  27654  noetainflem4  27658  etasslt  27731  cuteq1  27752  madebdaylemlrcut  27816  cutlt  27846  mulsuniflem  28058  bdayon  28179  om2noseqlt  28199  n0sfincut  28252  zs12ge0  28348  readdscl  28356  remulscl  28359  colinearalglem4  28842  axcontlem10  28906  upgrex  29025  smcnlem  30632  ubthlem1  30805  ubthlem3  30807  htthlem  30852  5oalem6  31594  leopmuli  32068  pjnormssi  32103  pjclem4  32134  pj3si  32142  hatomistici  32297  sumdmdlem  32353  sgn3da  32765  wrdt2ind  32881  xrge0tsmsd  33008  isarchiofld  33301  ordtrest2NEWlem  33918  qqhf  33982  eulerpartlemb  34365  ballotlemfc0  34490  ballotlemfcc  34491  subfacp1lem5  35171  erdszelem7  35184  erdszelem11  35188  pconnconn  35218  txpconn  35219  connpconn  35222  sconnpi1  35226  txsconn  35228  cvxsconn  35230  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem2  35269  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift2lem10  35299  cvmlift3lem4  35309  cvmlift3lem8  35313  satfun  35398  msubff1  35543  wzel  35807  wsuclem  35808  btwnouttr2  36005  cgrxfr  36038  btwnxfr  36039  brcolinear  36042  lineext  36059  btwnconn1lem13  36082  midofsegid  36087  segcon2  36088  brsegle  36091  seglecgr12im  36093  segletr  36097  colinbtwnle  36101  broutsideof2  36105  btwnoutside  36108  broutsideof3  36109  outsideoftr  36112  outsideofeq  36113  outsideofeu  36114  outsidele  36115  lineunray  36130  lineelsb2  36131  linethru  36136  finminlem  36301  nn0prpwlem  36305  neibastop2lem  36343  neibastop2  36344  neibastop3  36345  topjoin  36348  tailfb  36360  relowlssretop  37346  fvineqsneq  37395  wl-sbcom2d-lem1  37542  finixpnum  37594  poimirlem6  37615  poimirlem7  37616  poimirlem13  37622  poimirlem26  37635  poimirlem29  37638  heicant  37644  opnmbllem0  37645  mblfinlem3  37648  ismblfin  37650  ovoliunnfl  37651  voliunnfl  37653  volsupnfl  37654  itg2addnclem  37660  itg2addnclem3  37662  ftc1cnnc  37681  sdclem2  37731  fdc  37734  istotbnd3  37760  isbnd2  37772  isbnd3  37773  prdsbnd  37782  cntotbnd  37785  heibor1lem  37798  heibor1  37799  heiborlem10  37809  rrncmslem  37821  ghomco  37880  1idl  38015  unichnidl  38020  disjlem18  38787  prtlem10  38853  prtlem18  38865  atlatmstc  39307  cvrexchlem  39408  paddasslem14  39822  pexmidlem5N  39963  cdleme29ex  40363  cdlemefr29exN  40391  cdleme32fva  40426  diarnN  41118  dihlsscpre  41223  isnacs3  42691  fnwe2lem2  43033  kelac1  43045  hbtlem5  43110  hbt  43112  dgraa0p  43131  ofoafg  43336  ofoafo  43338  naddcnffo  43346  fzunt  43437  fzuntd  43438  monoordxrv  45470  rlimdmafv  47168  rlimdmafv2  47249  fmtnoprmfac2  47558  perfectALTVlem2  47713  mogoldbb  47776  lindslinindsimp2  48442