Theorem expdimp 457

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rexlimdvv  3219  rexlimdvvva  3221  ralcom2  3364  ssexnelpss  4070  sotr3  5610  wereu2  5658  oneqmini  6414  suctr  6449  onunel  6468  fiunlem  7938  poxp  8123  suppssr  8190  suppssrg  8191  smoel  8346  omabs  8636  omsmo  8643  iiner  8786  fodomr  9115  fisseneq  9222  suplub2  9420  supnub  9421  infglb  9450  infnlb  9452  inf3lem6  9601  cfcoflem  10255  coftr  10256  zorn2lem7  10485  alephreg  10566  inar1  10759  gruen  10796  letr  11303  lbzbi  12959  xrletr  13182  xmullem  13289  supxrun  13341  ssfzoulel  13788  ssfzo12bi  13789  hashbnd  14371  fi1uzind  14543  brfi1indALT  14546  cau3lem  15405  summo  15767  mertenslem2  15938  prodmolem2  15988  alzdvds  16377  nno  16439  nn0seqcvgd  16627  lcmdvds  16665  lcmf  16690  2mulprm  16750  divgcdodd  16768  prmpwdvds  16963  catpropd  17764  pltnle  18391  pltval3  18392  pltletr  18396  tsrlemax  18641  frgpnabllem1  19942  cyggexb  19968  rngcinv  20721  abvn0b  20918  isphld  21783  indistopon  23137  restntr  23318  cnprest  23425  lmss  23434  lmmo  23516  2ndcdisj  23592  txlm  23784  flftg  24132  bndth  25096  iscmet3  25431  bcthlem5  25466  ovolicc2lem4  25658  ellimc3  26017  lhop1  26152  ulmcaulem  26533  ulmcau  26534  ulmcn  26538  xrlimcnp  27109  nosepssdm  27826  ax5seglem4  29248  axcontlem2  29281  axcontlem4  29283  incistruhgr  29395  nbuhgr  29659  uhgrnbgr0nb  29670  wwlknp  30158  wwlksnred  30207  clwlkclwwlklem2a  30315  vdgn0frgrv2  30612  nmcvcn  31013  htthlem  31235  atcvat3i  32714  sumdmdlem2  32737  ifeqeqx  32854  bnj23  35073  bnj849  35279  prsrcmpltd  35435  cusgr3cyclex  35582  satffunlem2lem1  35850  funbreq  36216  cgrdegen  36450  lineext  36522  btwnconn1lem7  36539  btwnconn1lem14  36546  waj-ax  36869  lukshef-ax2  36870  relowlssretop  37953  finxpreclem6  37986  pibt2  38007  fin2solem  38201  poimirlem2  38217  poimirlem18  38233  poimirlem21  38236  poimirlem26  38241  poimirlem27  38242  poimirlem31  38246  unirep  38309  seqpo  38342  ssbnd  38383  intidl  38624  prnc  38662  eldisjlem19  39508  prtlem15  39595  lshpkrlem6  39835  atlatmstc  40039  cvrat3  40162  ps-2  40198  2lplnj  40340  paddasslem5  40544  dochkrshp4  42109  dvdsexpnn0  43041  rexlimdv3d  43362  isnacs3  43389  cantnfresb  43999  dflim5  44004  onmcl  44006  oaun3lem1  44049  pm14.24  45090  traxext  45634  rexlim2d  46289  iccpartigtl  48117  icceuelpartlem  48129  prproropf1olem4  48200  grimedg  48645  pgnbgreunbgrlem3  48828  pgnbgreunbgrlem6  48834  rngcinvALTV  48986  lindslinindsimp1  49182  lindslinindsimp2  49188  digexp  49332  aacllem  50546