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  696  pm5.6r  935  3expib  1233  sbiedh  1836  equs5  1878  moexexdc  2167  rsp2  2594  moi  3003  reu6  3009  sbciegft  3076  prel12  3880  opthpr  3881  invdisj  4107  sowlin  4446  reusv1  4584  relop  4910  elres  5079  iss  5089  funssres  5400  fv3  5698  funfvima  5923  poxp  6441  tfri3  6611  nndi  6732  nnmass  6733  nnmordi  6762  nnmord  6763  eroveu  6873  fiintim  7204  suplubti  7304  addnq0mo  7778  mulnq0mo  7779  prcdnql  7815  prcunqu  7816  prnmaxl  7819  prnminu  7820  genprndl  7852  genprndu  7853  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  recexprlemss1l  7966  recexprlemss1u  7967  addsrmo  8074  mulsrmo  8075  mulgt0sr  8109  ltleletr  8371  mulgt1  9154  fzind  9711  eqreznegel  9964  fzen  10397  elfzodifsumelfzo  10568  bernneq  11047  swrdswrdlem  11421  mulcn2  12022  prodmodclem2  12288  dvdsmod0  12504  divalglemeunn  12632  divalglemeuneg  12634  ndvdssub  12641  algcvgblem  12771  coprmdvds  12814  coprmdvds2  12815  divgcdcoprm0  12823  pceu  13018  dvdsprmpweqnn  13059  oddprmdvds  13077  infpnlem1  13082  imasaddfnlemg  13611  sgrpidmndm  13717  imasabl  14137  lmss  15223  lmtopcnp  15227  zabsle1  15984  2lgslem3  16086  uhgr2edg  16313  ushgredgedg  16333  ushgredgedgloop  16335  bj-sbimedh  16655  bj-nnen2lp  16836