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  4465  reusv1  4604  relop  4930  elres  5099  iss  5109  funssres  5420  fv3  5718  funfvima  5950  poxp  6468  tfri3  6638  nndi  6759  nnmass  6760  nnmordi  6789  nnmord  6790  eroveu  6900  fiintim  7238  suplubti  7341  addnq0mo  7815  mulnq0mo  7816  prcdnql  7852  prcunqu  7853  prnmaxl  7856  prnminu  7857  genprndl  7889  genprndu  7890  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  recexprlemss1l  8003  recexprlemss1u  8004  addsrmo  8111  mulsrmo  8112  mulgt0sr  8146  ltleletr  8408  mulgt1  9196  fzind  9766  eqreznegel  10024  fzen  10458  elfzodifsumelfzo  10630  bernneq  11112  swrdswrdlem  11491  mulcn2  12096  prodmodclem2  12362  dvdsmod0  12578  divalglemeunn  12706  divalglemeuneg  12708  ndvdssub  12715  algcvgblem  12845  coprmdvds  12888  coprmdvds2  12889  divgcdcoprm0  12897  pceu  13096  dvdsprmpweqnn  13137  oddprmdvds  13155  infpnlem1  13160  imasaddfnlemg  13686  sgrpidmndm  13784  imasabl  14191  lmss  15399  lmtopcnp  15403  zabsle1  16240  2lgslem3  16342  uhgr2edg  16569  ushgredgedg  16589  ushgredgedgloop  16591  bj-sbimedh  16921  bj-nnen2lp  17102