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  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2986  reu6  2992  sbciegft  3059  prel12  3849  opthpr  3850  invdisj  4076  sowlin  4412  reusv1  4550  relop  4875  elres  5044  iss  5054  funssres  5363  fv3  5655  funfvima  5878  poxp  6389  tfri3  6524  nndi  6645  nnmass  6646  nnmordi  6675  nnmord  6676  eroveu  6786  fiintim  7109  suplubti  7183  addnq0mo  7650  mulnq0mo  7651  prcdnql  7687  prcunqu  7688  prnmaxl  7691  prnminu  7692  genprndl  7724  genprndu  7725  distrlem1prl  7785  distrlem1pru  7786  distrlem5prl  7789  distrlem5pru  7790  recexprlemss1l  7838  recexprlemss1u  7839  addsrmo  7946  mulsrmo  7947  mulgt0sr  7981  ltleletr  8244  mulgt1  9026  fzind  9578  eqreznegel  9826  fzen  10256  elfzodifsumelfzo  10424  bernneq  10899  swrdswrdlem  11257  mulcn2  11844  prodmodclem2  12109  dvdsmod0  12325  divalglemeunn  12453  divalglemeuneg  12455  ndvdssub  12462  algcvgblem  12592  coprmdvds  12635  coprmdvds2  12636  divgcdcoprm0  12644  pceu  12839  dvdsprmpweqnn  12880  oddprmdvds  12898  infpnlem1  12903  imasaddfnlemg  13368  sgrpidmndm  13474  imasabl  13894  lmss  14941  lmtopcnp  14945  zabsle1  15699  2lgslem3  15801  uhgr2edg  16025  ushgredgedg  16045  ushgredgedgloop  16047  bj-sbimedh  16244  bj-nnen2lp  16426