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  2165  rsp2  2592  moi  2999  reu6  3005  sbciegft  3072  prel12  3874  opthpr  3875  invdisj  4101  sowlin  4440  reusv1  4578  relop  4904  elres  5073  iss  5083  funssres  5394  fv3  5692  funfvima  5917  poxp  6427  tfri3  6597  nndi  6718  nnmass  6719  nnmordi  6748  nnmord  6749  eroveu  6859  fiintim  7190  suplubti  7290  addnq0mo  7761  mulnq0mo  7762  prcdnql  7798  prcunqu  7799  prnmaxl  7802  prnminu  7803  genprndl  7835  genprndu  7836  distrlem1prl  7896  distrlem1pru  7897  distrlem5prl  7900  distrlem5pru  7901  recexprlemss1l  7949  recexprlemss1u  7950  addsrmo  8057  mulsrmo  8058  mulgt0sr  8092  ltleletr  8354  mulgt1  9136  fzind  9692  eqreznegel  9945  fzen  10376  elfzodifsumelfzo  10545  bernneq  11021  swrdswrdlem  11392  mulcn2  11993  prodmodclem2  12259  dvdsmod0  12475  divalglemeunn  12603  divalglemeuneg  12605  ndvdssub  12612  algcvgblem  12742  coprmdvds  12785  coprmdvds2  12786  divgcdcoprm0  12794  pceu  12989  dvdsprmpweqnn  13030  oddprmdvds  13048  infpnlem1  13053  imasaddfnlemg  13519  sgrpidmndm  13625  imasabl  14045  lmss  15103  lmtopcnp  15107  zabsle1  15864  2lgslem3  15966  uhgr2edg  16193  ushgredgedg  16213  ushgredgedgloop  16215  bj-sbimedh  16535  bj-nnen2lp  16716