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  7340  addnq0mo  7814  mulnq0mo  7815  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  genprndl  7888  genprndu  7889  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  recexprlemss1l  8002  recexprlemss1u  8003  addsrmo  8110  mulsrmo  8111  mulgt0sr  8145  ltleletr  8407  mulgt1  9194  fzind  9763  eqreznegel  10016  fzen  10449  elfzodifsumelfzo  10621  bernneq  11100  swrdswrdlem  11478  mulcn2  12080  prodmodclem2  12346  dvdsmod0  12562  divalglemeunn  12690  divalglemeuneg  12692  ndvdssub  12699  algcvgblem  12829  coprmdvds  12872  coprmdvds2  12873  divgcdcoprm0  12881  pceu  13076  dvdsprmpweqnn  13117  oddprmdvds  13135  infpnlem1  13140  imasaddfnlemg  13637  sgrpidmndm  13735  imasabl  14142  lmss  15349  lmtopcnp  15353  zabsle1  16130  2lgslem3  16232  uhgr2edg  16459  ushgredgedg  16479  ushgredgedgloop  16481  bj-sbimedh  16811  bj-nnen2lp  16992