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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2987  reu6  2993  sbciegft  3060  prel12  3852  opthpr  3853  invdisj  4079  sowlin  4415  reusv1  4553  relop  4878  elres  5047  iss  5057  funssres  5366  fv3  5658  funfvima  5881  poxp  6392  tfri3  6528  nndi  6649  nnmass  6650  nnmordi  6679  nnmord  6680  eroveu  6790  fiintim  7118  suplubti  7193  addnq0mo  7660  mulnq0mo  7661  prcdnql  7697  prcunqu  7698  prnmaxl  7701  prnminu  7702  genprndl  7734  genprndu  7735  distrlem1prl  7795  distrlem1pru  7796  distrlem5prl  7799  distrlem5pru  7800  recexprlemss1l  7848  recexprlemss1u  7849  addsrmo  7956  mulsrmo  7957  mulgt0sr  7991  ltleletr  8254  mulgt1  9036  fzind  9588  eqreznegel  9841  fzen  10271  elfzodifsumelfzo  10439  bernneq  10915  swrdswrdlem  11278  mulcn2  11866  prodmodclem2  12131  dvdsmod0  12347  divalglemeunn  12475  divalglemeuneg  12477  ndvdssub  12484  algcvgblem  12614  coprmdvds  12657  coprmdvds2  12658  divgcdcoprm0  12666  pceu  12861  dvdsprmpweqnn  12902  oddprmdvds  12920  infpnlem1  12925  imasaddfnlemg  13390  sgrpidmndm  13496  imasabl  13916  lmss  14963  lmtopcnp  14967  zabsle1  15721  2lgslem3  15823  uhgr2edg  16050  ushgredgedg  16070  ushgredgedgloop  16072  bj-sbimedh  16317  bj-nnen2lp  16499