Theorem expimpd 360

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

Hypothesis

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

Assertion

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

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 252	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  euotd  4176  swopo  4228  reusv3  4381  ralxfrd  4383  rexxfrd  4384  nlimsucg  4481  poirr2  4931  elpreima  5539  fmptco  5586  tposfo2  6164  nnm00  6425  th3qlem1  6531  fiintim  6817  supmoti  6880  infglbti  6912  infnlbti  6913  updjud  6967  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  uzind  9162  ledivge1le  9513  xltnegi  9618  ixxssixx  9685  expnegzap  10327  shftlem  10588  cau3lem  10886  caubnd2  10889  climuni  11062  2clim  11070  summodclem2  11151  summodc  11152  zsumdc  11153  fsumf1o  11159  fisumss  11161  fsumcl2lem  11167  fsumadd  11175  fsummulc2  11217  prodmodclem2  11346  prodmodc  11347  dfgcd2  11702  cncongrprm  11835  eltg3  12226  tgidm  12243  tgrest  12338  tgcn  12377  lmtopcnp  12419  txbasval  12436  txcnp  12440  bldisj  12570  xblm  12586  blssps  12596  blss  12597  blssexps  12598  blssex  12599  metcnp3  12680  bj-findis  13177