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  695  pm5.6r  934  3expib  1232  sbiedh  1835  equs5  1877  moexexdc  2164  rsp2  2582  moi  2989  reu6  2995  sbciegft  3062  prel12  3854  opthpr  3855  invdisj  4081  sowlin  4417  reusv1  4555  relop  4880  elres  5049  iss  5059  funssres  5369  fv3  5662  funfvima  5886  poxp  6397  tfri3  6533  nndi  6654  nnmass  6655  nnmordi  6684  nnmord  6685  eroveu  6795  fiintim  7123  suplubti  7199  addnq0mo  7667  mulnq0mo  7668  prcdnql  7704  prcunqu  7705  prnmaxl  7708  prnminu  7709  genprndl  7741  genprndu  7742  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  recexprlemss1l  7855  recexprlemss1u  7856  addsrmo  7963  mulsrmo  7964  mulgt0sr  7998  ltleletr  8261  mulgt1  9043  fzind  9595  eqreznegel  9848  fzen  10278  elfzodifsumelfzo  10447  bernneq  10923  swrdswrdlem  11289  mulcn2  11877  prodmodclem2  12143  dvdsmod0  12359  divalglemeunn  12487  divalglemeuneg  12489  ndvdssub  12496  algcvgblem  12626  coprmdvds  12669  coprmdvds2  12670  divgcdcoprm0  12678  pceu  12873  dvdsprmpweqnn  12914  oddprmdvds  12932  infpnlem1  12937  imasaddfnlemg  13402  sgrpidmndm  13508  imasabl  13928  lmss  14976  lmtopcnp  14980  zabsle1  15734  2lgslem3  15836  uhgr2edg  16063  ushgredgedg  16083  ushgredgedgloop  16085  bj-sbimedh  16393  bj-nnen2lp  16575