Theorem expdimp 451

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 414	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 405	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  rexlimdvv  3208  ralcom2  3371  ssexnelpss  4112  sotr3  5626  wereu2  5672  oneqmini  6415  suctr  6449  onunel  6468  fiunlem  7930  poxp  8116  suppssr  8183  suppssrg  8184  smoel  8362  omabs  8652  omsmo  8659  iiner  8785  fodomr  9130  fisseneq  9259  suplub2  9458  supnub  9459  infglb  9487  infnlb  9489  inf3lem6  9630  cfcoflem  10269  coftr  10270  zorn2lem7  10499  alephreg  10579  inar1  10772  gruen  10809  letr  11312  lbzbi  12924  xrletr  13141  xmullem  13247  supxrun  13299  ssfzoulel  13730  ssfzo12bi  13731  hashbnd  14300  fi1uzind  14462  brfi1indALT  14465  cau3lem  15305  summo  15667  mertenslem2  15835  prodmolem2  15883  alzdvds  16267  nno  16329  nn0seqcvgd  16511  lcmdvds  16549  lcmf  16574  2mulprm  16634  divgcdodd  16651  prmpwdvds  16841  catpropd  17657  pltnle  18295  pltval3  18296  pltletr  18300  tsrlemax  18543  frgpnabllem1  19782  cyggexb  19808  abvn0b  21120  isphld  21426  indistopon  22724  restntr  22906  cnprest  23013  lmss  23022  lmmo  23104  2ndcdisj  23180  txlm  23372  flftg  23720  bndth  24704  iscmet3  25041  bcthlem5  25076  ovolicc2lem4  25269  ellimc3  25628  lhop1  25766  ulmcaulem  26142  ulmcau  26143  ulmcn  26147  xrlimcnp  26709  nosepssdm  27425  ax5seglem4  28457  axcontlem2  28490  axcontlem4  28492  incistruhgr  28606  nbuhgr  28867  uhgrnbgr0nb  28878  wwlknp  29364  wwlksnred  29413  clwlkclwwlklem2a  29518  vdgn0frgrv2  29815  nmcvcn  30215  htthlem  30437  atcvat3i  31916  sumdmdlem2  31939  ifeqeqx  32041  bnj23  34027  bnj849  34234  prsrcmpltd  34384  cusgr3cyclex  34425  satffunlem2lem1  34693  funbreq  35045  cgrdegen  35280  lineext  35352  btwnconn1lem7  35369  btwnconn1lem14  35376  waj-ax  35602  lukshef-ax2  35603  relowlssretop  36547  finxpreclem6  36580  pibt2  36601  fin2solem  36777  poimirlem2  36793  poimirlem18  36809  poimirlem21  36812  poimirlem26  36817  poimirlem27  36818  poimirlem31  36822  unirep  36885  seqpo  36918  ssbnd  36959  intidl  37200  prnc  37238  eldisjlem19  37983  prtlem15  38048  lshpkrlem6  38288  atlatmstc  38492  cvrat3  38616  ps-2  38652  2lplnj  38794  paddasslem5  38998  dochkrshp4  40563  dvdsexpnn0  41534  rexlimdv3d  41723  isnacs3  41750  cantnfresb  42376  dflim5  42381  onmcl  42383  oaun3lem1  42426  pm14.24  43493  rexlim2d  44639  iccpartigtl  46389  icceuelpartlem  46401  prproropf1olem4  46472  rngcinv  46967  rngcinvALTV  46979  lindslinindsimp1  47225  lindslinindsimp2  47231  digexp  47380  aacllem  47935