Theorem impd 254

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		imp3.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3l 81	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 124	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  689  pm5.6r  927  3expib  1206  sbiedh  1787  equs5  1829  moexexdc  2110  rsp2  2527  moi  2920  reu6  2926  sbciegft  2993  prel12  3770  opthpr  3771  invdisj  3995  sowlin  4318  reusv1  4456  relop  4774  elres  4940  iss  4950  funssres  5255  fv3  5535  funfvima  5744  poxp  6228  tfri3  6363  nndi  6482  nnmass  6483  nnmordi  6512  nnmord  6513  eroveu  6621  fiintim  6923  suplubti  6994  addnq0mo  7441  mulnq0mo  7442  prcdnql  7478  prcunqu  7479  prnmaxl  7482  prnminu  7483  genprndl  7515  genprndu  7516  distrlem1prl  7576  distrlem1pru  7577  distrlem5prl  7580  distrlem5pru  7581  recexprlemss1l  7629  recexprlemss1u  7630  addsrmo  7737  mulsrmo  7738  mulgt0sr  7772  ltleletr  8033  mulgt1  8814  fzind  9362  eqreznegel  9608  fzen  10036  elfzodifsumelfzo  10194  bernneq  10633  mulcn2  11311  prodmodclem2  11576  dvdsmod0  11791  divalglemeunn  11916  divalglemeuneg  11918  ndvdssub  11925  algcvgblem  12039  coprmdvds  12082  coprmdvds2  12083  divgcdcoprm0  12091  pceu  12285  dvdsprmpweqnn  12325  oddprmdvds  12342  infpnlem1  12347  sgrpidmndm  12751  lmss  13528  lmtopcnp  13532  zabsle1  14182  bj-sbimedh  14294  bj-nnen2lp  14477