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  690  pm5.6r  928  3expib  1208  sbiedh  1801  equs5  1843  moexexdc  2129  rsp2  2547  moi  2947  reu6  2953  sbciegft  3020  prel12  3801  opthpr  3802  invdisj  4027  sowlin  4355  reusv1  4493  relop  4816  elres  4982  iss  4992  funssres  5300  fv3  5581  funfvima  5794  poxp  6290  tfri3  6425  nndi  6544  nnmass  6545  nnmordi  6574  nnmord  6575  eroveu  6685  fiintim  6992  suplubti  7066  addnq0mo  7514  mulnq0mo  7515  prcdnql  7551  prcunqu  7552  prnmaxl  7555  prnminu  7556  genprndl  7588  genprndu  7589  distrlem1prl  7649  distrlem1pru  7650  distrlem5prl  7653  distrlem5pru  7654  recexprlemss1l  7702  recexprlemss1u  7703  addsrmo  7810  mulsrmo  7811  mulgt0sr  7845  ltleletr  8108  mulgt1  8890  fzind  9441  eqreznegel  9688  fzen  10118  elfzodifsumelfzo  10277  bernneq  10752  mulcn2  11477  prodmodclem2  11742  dvdsmod0  11958  divalglemeunn  12086  divalglemeuneg  12088  ndvdssub  12095  algcvgblem  12217  coprmdvds  12260  coprmdvds2  12261  divgcdcoprm0  12269  pceu  12464  dvdsprmpweqnn  12505  oddprmdvds  12523  infpnlem1  12528  imasaddfnlemg  12957  sgrpidmndm  13061  imasabl  13466  lmss  14482  lmtopcnp  14486  zabsle1  15240  2lgslem3  15342  bj-sbimedh  15417  bj-nnen2lp  15600