Theorem impd 246

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 79	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 119	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 101

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104

This theorem is referenced by:  imp32  248  pm3.31  253  syland  281  imp4c  337  imp4d  338  imp5d  345  expimpd  349  expl  364  pm5.6r  845  3expib  1116  sbiedh  1684  equs5  1724  moexexdc  1998  rsp2  2386  moi  2744  reu6  2750  sbciegft  2813  prel12  3567  opthpr  3568  invdisj  3784  sowlin  4082  reusv1  4215  relop  4511  elres  4671  iss  4679  funssres  4967  fv3  5222  funfvima  5415  poxp  5878  tfri3  5981  nndi  6093  nnmass  6094  nnmordi  6117  nnmord  6118  eroveu  6225  addnq0mo  6573  mulnq0mo  6574  prcdnql  6610  prcunqu  6611  prnmaxl  6614  prnminu  6615  genprndl  6647  genprndu  6648  distrlem1prl  6708  distrlem1pru  6709  distrlem5prl  6712  distrlem5pru  6713  recexprlemss1l  6761  recexprlemss1u  6762  addsrmo  6856  mulsrmo  6857  mulgt0sr  6890  ltleletr  7129  mulgt1  7874  fzind  8382  eqreznegel  8616  fzen  8979  elfzodifsumelfzo  9129  bernneq  9501  mulcn2  10027  algcvgblem  10214  bj-sbimedh  10241  bj-nnen2lp  10409