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  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2986  reu6  2992  sbciegft  3059  prel12  3848  opthpr  3849  invdisj  4075  sowlin  4408  reusv1  4546  relop  4869  elres  5037  iss  5047  funssres  5356  fv3  5646  funfvima  5864  poxp  6368  tfri3  6503  nndi  6622  nnmass  6623  nnmordi  6652  nnmord  6653  eroveu  6763  fiintim  7081  suplubti  7155  addnq0mo  7622  mulnq0mo  7623  prcdnql  7659  prcunqu  7660  prnmaxl  7663  prnminu  7664  genprndl  7696  genprndu  7697  distrlem1prl  7757  distrlem1pru  7758  distrlem5prl  7761  distrlem5pru  7762  recexprlemss1l  7810  recexprlemss1u  7811  addsrmo  7918  mulsrmo  7919  mulgt0sr  7953  ltleletr  8216  mulgt1  8998  fzind  9550  eqreznegel  9797  fzen  10227  elfzodifsumelfzo  10394  bernneq  10869  swrdswrdlem  11222  mulcn2  11809  prodmodclem2  12074  dvdsmod0  12290  divalglemeunn  12418  divalglemeuneg  12420  ndvdssub  12427  algcvgblem  12557  coprmdvds  12600  coprmdvds2  12601  divgcdcoprm0  12609  pceu  12804  dvdsprmpweqnn  12845  oddprmdvds  12863  infpnlem1  12868  imasaddfnlemg  13333  sgrpidmndm  13439  imasabl  13859  lmss  14905  lmtopcnp  14909  zabsle1  15663  2lgslem3  15765  uhgr2edg  15989  ushgredgedg  16009  ushgredgedgloop  16011  bj-sbimedh  16065  bj-nnen2lp  16247