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  689  pm5.6r  927  3expib  1206  sbiedh  1787  equs5  1829  moexexdc  2110  rsp2  2527  moi  2920  reu6  2926  sbciegft  2993  prel12  3771  opthpr  3772  invdisj  3997  sowlin  4320  reusv1  4458  relop  4777  elres  4943  iss  4953  funssres  5258  fv3  5538  funfvima  5748  poxp  6232  tfri3  6367  nndi  6486  nnmass  6487  nnmordi  6516  nnmord  6517  eroveu  6625  fiintim  6927  suplubti  6998  addnq0mo  7445  mulnq0mo  7446  prcdnql  7482  prcunqu  7483  prnmaxl  7486  prnminu  7487  genprndl  7519  genprndu  7520  distrlem1prl  7580  distrlem1pru  7581  distrlem5prl  7584  distrlem5pru  7585  recexprlemss1l  7633  recexprlemss1u  7634  addsrmo  7741  mulsrmo  7742  mulgt0sr  7776  ltleletr  8038  mulgt1  8819  fzind  9367  eqreznegel  9613  fzen  10042  elfzodifsumelfzo  10200  bernneq  10640  mulcn2  11319  prodmodclem2  11584  dvdsmod0  11799  divalglemeunn  11925  divalglemeuneg  11927  ndvdssub  11934  algcvgblem  12048  coprmdvds  12091  coprmdvds2  12092  divgcdcoprm0  12100  pceu  12294  dvdsprmpweqnn  12334  oddprmdvds  12351  infpnlem1  12356  imasaddfnlemg  12734  sgrpidmndm  12820  lmss  13682  lmtopcnp  13686  zabsle1  14336  bj-sbimedh  14459  bj-nnen2lp  14642