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  2140  rsp2  2558  moi  2964  reu6  2970  sbciegft  3037  prel12  3826  opthpr  3827  invdisj  4053  sowlin  4386  reusv1  4524  relop  4847  elres  5015  iss  5025  funssres  5333  fv3  5623  funfvima  5841  poxp  6343  tfri3  6478  nndi  6597  nnmass  6598  nnmordi  6627  nnmord  6628  eroveu  6738  fiintim  7056  suplubti  7130  addnq0mo  7597  mulnq0mo  7598  prcdnql  7634  prcunqu  7635  prnmaxl  7638  prnminu  7639  genprndl  7671  genprndu  7672  distrlem1prl  7732  distrlem1pru  7733  distrlem5prl  7736  distrlem5pru  7737  recexprlemss1l  7785  recexprlemss1u  7786  addsrmo  7893  mulsrmo  7894  mulgt0sr  7928  ltleletr  8191  mulgt1  8973  fzind  9525  eqreznegel  9772  fzen  10202  elfzodifsumelfzo  10369  bernneq  10844  swrdswrdlem  11197  mulcn2  11784  prodmodclem2  12049  dvdsmod0  12265  divalglemeunn  12393  divalglemeuneg  12395  ndvdssub  12402  algcvgblem  12532  coprmdvds  12575  coprmdvds2  12576  divgcdcoprm0  12584  pceu  12779  dvdsprmpweqnn  12820  oddprmdvds  12838  infpnlem1  12843  imasaddfnlemg  13307  sgrpidmndm  13413  imasabl  13833  lmss  14879  lmtopcnp  14883  zabsle1  15637  2lgslem3  15739  uhgr2edg  15961  bj-sbimedh  16015  bj-nnen2lp  16197