Theorem expdimp 458

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

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

Assertion

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

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		expdimp.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 412	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rexlimdvv  3218  rexlimdvvva  3220  ralcom2  3362  ssexnelpss  4044  prsrcmpltd  4432  sotr3  5599  wereu2  5647  oneqmini  6416  suctr  6451  onunel  6470  fiunlem  7954  poxp  8140  suppssr  8212  suppssrg  8213  smoel  8368  omabs  8660  omsmo  8667  iiner  8810  fodomr  9147  fisseneq  9254  suplub2  9453  supnub  9454  infglb  9483  infnlb  9485  inf3lem6  9634  cfcoflem  10350  coftr  10351  zorn2lem7  10580  alephreg  10667  inar1  10860  gruen  10897  letr  11404  lbzbi  13063  xrletr  13287  xmullem  13394  supxrun  13446  ssfzoulel  13895  ssfzo12bi  13896  hashbnd  14480  fi1uzind  14652  brfi1indALT  14655  cau3lem  15522  summo  15883  mertenslem2  16054  prodmolem2  16102  alzdvds  16490  nno  16552  nn0seqcvgd  16745  lcmdvds  16783  lcmf  16808  2mulprm  16868  divgcdodd  16886  prmpwdvds  17082  catpropd  17883  pltnle  18510  pltval3  18511  pltletr  18515  tsrlemax  18760  frgpnabllem1  20087  cyggexb  20113  rngcinv  20889  abvn0b  21093  isphld  21960  indistopon  23319  restntr  23500  cnprest  23607  lmss  23616  lmmo  23698  2ndcdisj  23775  txlm  23967  flftg  24315  bndth  25279  iscmet3  25614  bcthlem5  25649  ovolicc2lem4  25841  ellimc3  26199  lhop1  26334  ulmcaulem  26721  ulmcau  26722  ulmcn  26726  xrlimcnp  27296  nosepssdm  28043  ax5seglem4  29510  axcontlem2  29543  axcontlem4  29545  incistruhgr  29657  nbuhgr  29924  uhgrnbgr0nb  29935  wwlknp  30432  wwlksnred  30481  clwlkclwwlklem2a  30589  vdgn0frgrv2  30896  nmcvcn  31297  htthlem  31519  atcvat3i  32998  sumdmdlem2  33021  ifeqeqx  33180  bnj23  35391  bnj849  35597  cusgr3cyclex  35953  satffunlem2lem1  36211  funbreq  36576  cgrdegen  36811  lineext  36883  btwnconn1lem7  36900  btwnconn1lem14  36907  waj-ax  37244  lukshef-ax2  37245  relowlssretop  38329  finxpreclem6  38362  pibt2  38383  fin2solem  38572  poimirlem2  38583  poimirlem18  38599  poimirlem21  38602  poimirlem26  38607  poimirlem27  38608  poimirlem31  38612  unirep  38691  seqpo  38724  ssbnd  38765  intidl  39006  prnc  39044  eldisjlem19  39888  prtlem15  39975  lshpkrlem6  40215  atlatmstc  40419  cvrat3  40542  ps-2  40578  2lplnj  40720  paddasslem5  40924  dochkrshp4  42489  dvdsexpnn0  43429  rexlimdv3d  43736  isnacs3  43764  cantnfresb  44369  dflim5  44374  onmcl  44376  oaun3lem1  44419  pm14.24  45459  traxext  46010  rexlim2d  46680  iccpartigtl  48548  icceuelpartlem  48560  prproropf1olem4  48631  grimedg  49076  pgnbgreunbgrlem3  49259  pgnbgreunbgrlem6  49265  rngcinvALTV  49416  lindslinindsimp1  49612  lindslinindsimp2  49618  digexp  49762  aacllem  50982