Theorem impd 252

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 123	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  291  imp4c  349  imp4d  350  imp5d  357  expimpd  361  expl  376  pm3.37  679  pm5.6r  913  3expib  1185  sbiedh  1761  equs5  1802  moexexdc  2084  rsp2  2485  moi  2871  reu6  2877  sbciegft  2943  prel12  3706  opthpr  3707  invdisj  3931  sowlin  4250  reusv1  4387  relop  4697  elres  4863  iss  4873  funssres  5173  fv3  5452  funfvima  5657  poxp  6137  tfri3  6272  nndi  6390  nnmass  6391  nnmordi  6420  nnmord  6421  eroveu  6528  fiintim  6825  suplubti  6895  addnq0mo  7279  mulnq0mo  7280  prcdnql  7316  prcunqu  7317  prnmaxl  7320  prnminu  7321  genprndl  7353  genprndu  7354  distrlem1prl  7414  distrlem1pru  7415  distrlem5prl  7418  distrlem5pru  7419  recexprlemss1l  7467  recexprlemss1u  7468  addsrmo  7575  mulsrmo  7576  mulgt0sr  7610  ltleletr  7870  mulgt1  8645  fzind  9190  eqreznegel  9433  fzen  9854  elfzodifsumelfzo  10009  bernneq  10443  mulcn2  11113  prodmodclem2  11378  divalglemeunn  11654  divalglemeuneg  11656  ndvdssub  11663  algcvgblem  11766  coprmdvds  11809  coprmdvds2  11810  divgcdcoprm0  11818  lmss  12454  lmtopcnp  12458  bj-sbimedh  13149  bj-nnen2lp  13323