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  1798  equs5  1840  moexexdc  2126  rsp2  2544  moi  2944  reu6  2950  sbciegft  3017  prel12  3798  opthpr  3799  invdisj  4024  sowlin  4352  reusv1  4490  relop  4813  elres  4979  iss  4989  funssres  5297  fv3  5578  funfvima  5791  poxp  6287  tfri3  6422  nndi  6541  nnmass  6542  nnmordi  6571  nnmord  6572  eroveu  6682  fiintim  6987  suplubti  7061  addnq0mo  7509  mulnq0mo  7510  prcdnql  7546  prcunqu  7547  prnmaxl  7550  prnminu  7551  genprndl  7583  genprndu  7584  distrlem1prl  7644  distrlem1pru  7645  distrlem5prl  7648  distrlem5pru  7649  recexprlemss1l  7697  recexprlemss1u  7698  addsrmo  7805  mulsrmo  7806  mulgt0sr  7840  ltleletr  8103  mulgt1  8884  fzind  9435  eqreznegel  9682  fzen  10112  elfzodifsumelfzo  10271  bernneq  10734  mulcn2  11458  prodmodclem2  11723  dvdsmod0  11939  divalglemeunn  12065  divalglemeuneg  12067  ndvdssub  12074  algcvgblem  12190  coprmdvds  12233  coprmdvds2  12234  divgcdcoprm0  12242  pceu  12436  dvdsprmpweqnn  12477  oddprmdvds  12495  infpnlem1  12500  imasaddfnlemg  12900  sgrpidmndm  13004  imasabl  13409  lmss  14425  lmtopcnp  14429  zabsle1  15156  2lgslem3  15258  bj-sbimedh  15333  bj-nnen2lp  15516