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  700  pm5.6r  939  3expib  1237  sbiedh  1840  equs5  1882  moexexdc  2171  rsp2  2600  moi  3009  reu6  3015  sbciegft  3082  prel12  3894  opthpr  3895  invdisj  4121  sowlin  4463  reusv1  4602  relop  4928  elres  5097  iss  5107  funssres  5418  fv3  5716  funfvima  5944  poxp  6462  tfri3  6632  nndi  6753  nnmass  6754  nnmordi  6783  nnmord  6784  eroveu  6894  fiintim  7232  suplubti  7334  addnq0mo  7808  mulnq0mo  7809  prcdnql  7845  prcunqu  7846  prnmaxl  7849  prnminu  7850  genprndl  7882  genprndu  7883  distrlem1prl  7943  distrlem1pru  7944  distrlem5prl  7947  distrlem5pru  7948  recexprlemss1l  7996  recexprlemss1u  7997  addsrmo  8104  mulsrmo  8105  mulgt0sr  8139  ltleletr  8401  mulgt1  9187  fzind  9744  eqreznegel  9997  fzen  10430  elfzodifsumelfzo  10602  bernneq  11081  swrdswrdlem  11459  mulcn2  12061  prodmodclem2  12327  dvdsmod0  12543  divalglemeunn  12671  divalglemeuneg  12673  ndvdssub  12680  algcvgblem  12810  coprmdvds  12853  coprmdvds2  12854  divgcdcoprm0  12862  pceu  13057  dvdsprmpweqnn  13098  oddprmdvds  13116  infpnlem1  13121  imasaddfnlemg  13618  sgrpidmndm  13716  imasabl  14123  lmss  15330  lmtopcnp  15334  zabsle1  16101  2lgslem3  16203  uhgr2edg  16430  ushgredgedg  16450  ushgredgedgloop  16452  bj-sbimedh  16782  bj-nnen2lp  16963