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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  700  pm5.6r  939  3expib  1237  sbiedh  1840  equs5  1882  moexexdc  2171  rsp2  2600  moi  3009  reu6  3015  sbciegft  3082  prel12  3896  opthpr  3897  invdisj  4123  sowlin  4467  reusv1  4606  relop  4932  elres  5101  iss  5112  funssres  5423  fv3  5721  funfvima  5953  poxp  6472  tfri3  6643  nndi  6764  nnmass  6765  nnmordi  6794  nnmord  6795  eroveu  6905  fiintim  7244  suplubti  7347  addnq0mo  7821  mulnq0mo  7822  prcdnql  7858  prcunqu  7859  prnmaxl  7862  prnminu  7863  genprndl  7895  genprndu  7896  distrlem1prl  7956  distrlem1pru  7957  distrlem5prl  7960  distrlem5pru  7961  recexprlemss1l  8009  recexprlemss1u  8010  addsrmo  8117  mulsrmo  8118  mulgt0sr  8152  ltleletr  8414  mulgt1  9202  fzind  9772  eqreznegel  10030  fzen  10464  elfzodifsumelfzo  10636  bernneq  11119  swrdswrdlem  11498  mulcn2  12103  prodmodclem2  12369  dvdsmod0  12585  divalglemeunn  12713  divalglemeuneg  12715  ndvdssub  12722  algcvgblem  12852  coprmdvds  12895  coprmdvds2  12896  divgcdcoprm0  12904  pceu  13103  dvdsprmpweqnn  13144  oddprmdvds  13162  infpnlem1  13167  imasaddfnlemg  13694  sgrpidmndm  13792  imasabl  14230  lmss  15505  lmtopcnp  15509  zabsle1  16356  2lgslem3  16458  uhgr2edg  16685  ushgredgedg  16705  ushgredgedgloop  16707  bj-sbimedh  17037  bj-nnen2lp  17218