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  1835  equs5  1877  moexexdc  2164  rsp2  2583  moi  2990  reu6  2996  sbciegft  3063  prel12  3859  opthpr  3860  invdisj  4086  sowlin  4423  reusv1  4561  relop  4886  elres  5055  iss  5065  funssres  5376  fv3  5671  funfvima  5896  poxp  6406  tfri3  6576  nndi  6697  nnmass  6698  nnmordi  6727  nnmord  6728  eroveu  6838  fiintim  7166  suplubti  7242  addnq0mo  7710  mulnq0mo  7711  prcdnql  7747  prcunqu  7748  prnmaxl  7751  prnminu  7752  genprndl  7784  genprndu  7785  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  recexprlemss1l  7898  recexprlemss1u  7899  addsrmo  8006  mulsrmo  8007  mulgt0sr  8041  ltleletr  8304  mulgt1  9086  fzind  9638  eqreznegel  9891  fzen  10321  elfzodifsumelfzo  10490  bernneq  10966  swrdswrdlem  11332  mulcn2  11933  prodmodclem2  12199  dvdsmod0  12415  divalglemeunn  12543  divalglemeuneg  12545  ndvdssub  12552  algcvgblem  12682  coprmdvds  12725  coprmdvds2  12726  divgcdcoprm0  12734  pceu  12929  dvdsprmpweqnn  12970  oddprmdvds  12988  infpnlem1  12993  imasaddfnlemg  13458  sgrpidmndm  13564  imasabl  13984  lmss  15037  lmtopcnp  15041  zabsle1  15798  2lgslem3  15900  uhgr2edg  16127  ushgredgedg  16147  ushgredgedgloop  16149  bj-sbimedh  16469  bj-nnen2lp  16650