Theorem a2d 26

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
a2d	⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		ax-2 7	. 2 ⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
3	1, 2	syl 14	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  561  cbv1  1794  cbv1v  1796  ralimdaa  2610  reuss2  3505  finds2  4728  ssrel  4843  ssrel2  4845  ssrelrel  4855  funfvima2  5924  tfrlem1  6552  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfri3  6611  nneneq  7124  ac6sfi  7168  nnnninfeq  7432  nnnninfeq2  7433  pitonn  8179  nnaddcl  9277  nnmulcl  9278  zaddcllempos  9634  zaddcllemneg  9636  peano5uzti  9707  uzind2  9711  fzind  9714  zindd  9717  uzaddcl  9939  exfzdc  10611  frec2uzltd  10792  frecuzrdgg  10805  seq3val  10849  seqvalcd  10850  seq3clss  10860  monoord  10874  seq3caopr3  10880  seqcaopr3g  10881  seq3f1olemp  10904  seqf1oglem2a  10907  seqf1og  10910  seq3id3  10913  seq3homo  10916  seq3z  10917  seqfeq4g  10920  ser3ge0  10925  exp3vallem  10929  expcllem  10939  expap0  10958  mulexp  10967  expadd  10970  expmul  10973  leexp2r  10982  leexp1a  10983  bernneq  11050  modqexp  11056  nn0ltexp2  11099  apexp1  11108  facdiv  11128  facwordi  11130  faclbnd  11131  faclbnd6  11134  omgadd  11194  hashmap  11220  seq3coll  11242  cjexp  11606  resqrexlemover  11723  resqrexlemdecn  11725  resqrexlemlo  11726  resqrexlemcalc3  11729  absexp  11792  fsum2d  12149  modfsummod  12172  fsumabs  12179  fsumiun  12191  binom  12198  bcxmas  12203  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  clim2prod  12253  prodfap0  12259  prodfrecap  12260  fprodabs  12330  fprod2d  12337  demoivreALT  12488  dvdsfac  12574  bitsinv1  12676  gcdmultiple  12744  rplpwr  12751  nn0seqcvgd  12766  alginv  12772  algcvga  12776  algfx  12777  prmdvdsexp  12873  prmfac1  12877  eulerthlemrprm  12954  eulerthlema  12955  pcmpt  13069  pcfac  13076  prmpwdvds  13081  ennnfoneleminc  13249  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemhom  13253  nninfdclemlt  13289  gsumfzz  13753  mulgnnass  13913  mhmmulg  13919  gsumfzconst  14097  srgmulgass  14235  srgpcomp  14236  lmodvsmmulgdi  14600  cnfldexp  14854  gsumfzfsumlemm  14864  tgcl  15058  dvmptfsum  15719  plycolemc  15752  rpcxpmul2  15907  lgsquad2lem2  16084  eupth2lemsfi  16602  eupth2fi  16603  depindlem2  16631  depindlem3  16632  nninfsellemdc  16927  nnnninfex  16939