Theorem impd 242

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 75	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 115	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 27	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  imp32  244  pm3.31  249  syland  277  imp4c  333  imp4d  334  imp5d  341  expimpd  345  expl  360  pm5.6r  836  3expib  1107  sbiedh  1670  equs5  1710  moexexdc  1984  rsp2  2371  moi  2724  reu6  2730  sbciegft  2793  prel12  3542  opthpr  3543  invdisj  3759  sowlin  4057  reusv1  4190  relop  4486  elres  4646  iss  4654  funssres  4942  fv3  5197  funfvima  5390  poxp  5853  tfri3  5953  nndi  6065  nnmass  6066  nnmordi  6089  nnmord  6090  eroveu  6197  addnq0mo  6545  mulnq0mo  6546  prcdnql  6582  prcunqu  6583  prnmaxl  6586  prnminu  6587  genprndl  6619  genprndu  6620  distrlem1prl  6680  distrlem1pru  6681  distrlem5prl  6684  distrlem5pru  6685  recexprlemss1l  6733  recexprlemss1u  6734  addsrmo  6828  mulsrmo  6829  mulgt0sr  6862  ltleletr  7100  mulgt1  7829  fzind  8353  eqreznegel  8549  fzen  8907  elfzodifsumelfzo  9057  bernneq  9369  mulcn2  9833  algcvgblem  9888  bj-sbimedh  9911  bj-nnen2lp  10079