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  2922  reu6  2928  sbciegft  2995  prel12  3773  opthpr  3774  invdisj  3999  sowlin  4322  reusv1  4460  relop  4779  elres  4945  iss  4955  funssres  5260  fv3  5540  funfvima  5750  poxp  6235  tfri3  6370  nndi  6489  nnmass  6490  nnmordi  6519  nnmord  6520  eroveu  6628  fiintim  6930  suplubti  7001  addnq0mo  7448  mulnq0mo  7449  prcdnql  7485  prcunqu  7486  prnmaxl  7489  prnminu  7490  genprndl  7522  genprndu  7523  distrlem1prl  7583  distrlem1pru  7584  distrlem5prl  7587  distrlem5pru  7588  recexprlemss1l  7636  recexprlemss1u  7637  addsrmo  7744  mulsrmo  7745  mulgt0sr  7779  ltleletr  8041  mulgt1  8822  fzind  9370  eqreznegel  9616  fzen  10045  elfzodifsumelfzo  10203  bernneq  10643  mulcn2  11322  prodmodclem2  11587  dvdsmod0  11802  divalglemeunn  11928  divalglemeuneg  11930  ndvdssub  11937  algcvgblem  12051  coprmdvds  12094  coprmdvds2  12095  divgcdcoprm0  12103  pceu  12297  dvdsprmpweqnn  12337  oddprmdvds  12354  infpnlem1  12359  imasaddfnlemg  12740  sgrpidmndm  12826  lmss  13785  lmtopcnp  13789  zabsle1  14439  bj-sbimedh  14562  bj-nnen2lp  14745