Theorem expdimp 452

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

Hypothesis

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

Assertion

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

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 451	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 444	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  rexlimdvv  3019  ralcom2  3083  ssexnelpss  3682  wereu2  5035  oneqmini  5693  suctr  5725  fun11iun  7019  poxp  7176  suppssr  7213  smoel  7344  omabs  7614  omsmo  7621  iiner  7706  fodomr  7996  fisseneq  8056  suplub2  8250  supnub  8251  infglb  8279  infnlb  8281  inf3lem6  8413  cfcoflem  8977  coftr  8978  zorn2lem7  9207  alephreg  9283  inar1  9476  gruen  9513  letr  10010  lbzbi  11652  xrletr  11865  xmullem  11966  supxrun  12018  ssfzoulel  12428  ssfzo12bi  12429  hashbnd  12985  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  cau3lem  13942  summo  14295  mertenslem2  14456  prodmolem2  14504  alzdvds  14880  nno  14936  nn0seqcvgd  15121  lcmdvds  15159  lcmf  15184  divgcdodd  15260  prmpwdvds  15446  catpropd  16192  pltnle  16789  pltval3  16790  pltletr  16794  tsrlemax  17043  frgpnabllem1  18099  cyggexb  18123  abvn0b  19123  isphld  19818  indistopon  20615  restntr  20796  cnprest  20903  lmss  20912  lmmo  20994  2ndcdisj  21069  txlm  21261  flftg  21610  bndth  22565  iscmet3  22899  bcthlem5  22933  ovolicc2lem4  23095  ellimc3  23449  lhop1  23581  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  xrlimcnp  24495  ax5seglem4  25612  axcontlem2  25645  axcontlem4  25647  incistruhgr  25746  clwlkisclwwlklem2a  26313  rusgrasn  26472  frgrawopreglem5  26575  extwwlkfablem2  26605  nmcvcn  26934  htthlem  27158  atcvat3i  28639  sumdmdlem2  28662  ifeqeqx  28745  bnj23  30038  bnj849  30249  funbreq  30914  sltasym  31071  cgrdegen  31281  lineext  31353  btwnconn1lem7  31370  btwnconn1lem14  31377  waj-ax  31583  lukshef-ax2  31584  relowlssretop  32387  finxpreclem6  32409  fin2solem  32565  poimirlem2  32581  poimirlem18  32597  poimirlem21  32600  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  unirep  32677  seqpo  32713  ssbnd  32757  intidl  32998  prnc  33036  prtlem15  33178  lshpkrlem6  33420  atlatmstc  33624  cvrat3  33746  ps-2  33782  2lplnj  33924  paddasslem5  34128  dochkrshp4  35696  isnacs3  36291  pm14.24  37655  rexlim2d  38692  iccpartigtl  39961  icceuelpartlem  39973  nbuhgr  40565  uhgrnbgr0nb  40576  wwlknp  41045  wwlksnred  41098  clwlkclwwlklem2a  41207  vdgn0frgrv2  41465  frgrwopreglem5  41485  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  lindslinindsimp1  42040  lindslinindsimp2  42046  digexp  42199  aacllem  42356