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  691  pm5.6r  929  3expib  1209  sbiedh  1811  equs5  1853  moexexdc  2139  rsp2  2557  moi  2960  reu6  2966  sbciegft  3033  prel12  3817  opthpr  3818  invdisj  4043  sowlin  4374  reusv1  4512  relop  4835  elres  5003  iss  5013  funssres  5321  fv3  5611  funfvima  5828  poxp  6330  tfri3  6465  nndi  6584  nnmass  6585  nnmordi  6614  nnmord  6615  eroveu  6725  fiintim  7042  suplubti  7116  addnq0mo  7575  mulnq0mo  7576  prcdnql  7612  prcunqu  7613  prnmaxl  7616  prnminu  7617  genprndl  7649  genprndu  7650  distrlem1prl  7710  distrlem1pru  7711  distrlem5prl  7714  distrlem5pru  7715  recexprlemss1l  7763  recexprlemss1u  7764  addsrmo  7871  mulsrmo  7872  mulgt0sr  7906  ltleletr  8169  mulgt1  8951  fzind  9503  eqreznegel  9750  fzen  10180  elfzodifsumelfzo  10347  bernneq  10822  swrdswrdlem  11175  mulcn2  11693  prodmodclem2  11958  dvdsmod0  12174  divalglemeunn  12302  divalglemeuneg  12304  ndvdssub  12311  algcvgblem  12441  coprmdvds  12484  coprmdvds2  12485  divgcdcoprm0  12493  pceu  12688  dvdsprmpweqnn  12729  oddprmdvds  12747  infpnlem1  12752  imasaddfnlemg  13216  sgrpidmndm  13322  imasabl  13742  lmss  14788  lmtopcnp  14792  zabsle1  15546  2lgslem3  15648  bj-sbimedh  15841  bj-nnen2lp  16024